for i, j being Nat st i,j are_coprime holds
i lcm j = i * j