let m, n be Nat; :: thesis: m gcd (m lcm n) = (n gcd m) lcm m
m gcd (m lcm n) = m by Th67;
hence m gcd (m lcm n) = (n gcd m) lcm m by Th66; :: thesis: verum