theorem :: PEPIN:1

for i being Nat holds i,i + 1 are_coprime