theorem MT: :: NEWTON06:56

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