theorem Th45: :: NEWTON02:143

for a, b, m being Nat st a <> 0 holds
((a,b) In_Power m) . 1 <> 0