for a, b being Nat
for m being non zero Nat holds
( a = 0 iff ((a,b) In_Power m) . 1 = 0 )