for l being natural non zero number holds
( Fermat l is prime iff 3 |^ (((Fermat l) - 1) / 2), - 1 are_congruent_mod Fermat l )