let a, b, k, l be Nat; :: thesis: ( a > 0 & a = (a gcd b) * k & b = (a gcd b) * l implies k gcd l = 1 )

assume A1: ( a > 0 & a = (a gcd b) * k & b = (a gcd b) * l ) ; :: thesis: k gcd l = 1

then A2: a gcd b > 0 ;

k > 0 by A1;

then (a gcd b) * 1 = (a gcd b) * (k gcd l) by A1, EULER_1:15;

hence k gcd l = 1 by XCMPLX_1:5, A2; :: thesis: verum

assume A1: ( a > 0 & a = (a gcd b) * k & b = (a gcd b) * l ) ; :: thesis: k gcd l = 1

then A2: a gcd b > 0 ;

k > 0 by A1;

then (a gcd b) * 1 = (a gcd b) * (k gcd l) by A1, EULER_1:15;

hence k gcd l = 1 by XCMPLX_1:5, A2; :: thesis: verum