for x being odd Integer
for k being Nat st k >= 3 holds
(x |^ (2 |^ (k -' 2))) mod (2 |^ k) = 1