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