let a, b, c, d be Nat; :: thesis: ( a,b are_coprime & a * b = c * d implies a * b = (((a gcd c) * (b gcd c)) * (a gcd d)) * (b gcd d) )
assume A1: a,b are_coprime ; :: thesis: ( not a * b = c * d or a * b = (((a gcd c) * (b gcd c)) * (a gcd d)) * (b gcd d) )
assume A2: a * b = c * d ; :: thesis: a * b = (((a gcd c) * (b gcd c)) * (a gcd d)) * (b gcd d)
then ( c divides a * b & d divides a * b ) ;
then ( (a gcd c) * (b gcd c) = c & (a gcd d) * (b gcd d) = d ) by A1, CDN;
hence a * b = (((a gcd c) * (b gcd c)) * (a gcd d)) * (b gcd d) by A2; :: thesis: verum