theorem :: NEWTON03:84

for a being non trivial Nat
for b, c being non zero Integer st a |^ (a |-count b) divides c & a |^ (a |-count c) divides b holds
a |-count b = a |-count c