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