theorem COM: :: NEWTON06:31

for a, b being Nat st a,b are_coprime holds
for n being non trivial Nat holds max ((a mod n),(b mod n)) > 0