theorem DN: :: NEWTON03:86

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