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