theorem :: NEWTON05:18

for a, b being Nat
for c being non zero Nat st (a mod c) * (b mod c) >= c holds
a mod c > 1