for n1, n2, n3 being non zero Nat holds (n1 gcd n3) lcm (n2 gcd n3) = (n1 lcm n2) gcd n3