theorem Th6: :: PEPIN:6

for i, n being Nat st i <> 0 holds
( i divides n iff n mod i = 0 )