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