theorem Th47: :: PEPIN:47

for i, n, p being Nat st p > 1 & (i |^ n) mod p = 1 & i,p are_coprime holds
order (i,p) divides n