theorem Th49: :: PEPIN:49

for i, p being Nat st p is prime & i,p are_coprime holds
order (i,p) divides p -' 1