let a, b be Nat; :: thesis: ( not a,b are_coprime implies a * b is square-containing )
assume not a,b are_coprime ; :: thesis: a * b is square-containing

per cases then ( a gcd b < 1 or a gcd b > 1 ) by XXREAL_0:1;

suppose a gcd b < 1 ; :: thesis: a * b is square-containing

then ( a = 0 & b = 0 ) by NAT_1:14;
hence a * b is square-containing ; :: thesis: verum

end;

suppose a gcd b > 1 ; :: thesis: a * b is square-containing

then not a gcd b is trivial ;
then reconsider k = (a gcd b) |^ 2 as non trivial square Nat ;
reconsider l = (a lcm b) / (a gcd b) as Nat ;
a * b = k * l by Th13;
hence a * b is square-containing ; :: thesis: verum

end;

end;