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