for a, b being Nat st b <> 1 & a <> 0 & b divides b |^ (b |-count a) holds
b divides a