theorem :: NUMBER12:13

for n being non zero Nat holds n, Fermat n are_coprime by T51;