let a, b be non zero Nat; :: thesis: a / (a gcd b) = (a lcm b) / b
a / (a gcd b) = (a * b) / (b * (a gcd b)) by XCMPLX_1:91
.= ((a gcd b) * (a lcm b)) / (b * (a gcd b)) by NAT_D:29
.= (a lcm b) / b by XCMPLX_1:91 ;
hence a / (a gcd b) = (a lcm b) / b ; :: thesis: verum