theorem :: PEPIN:64

for i, n being Nat st n > 0 holds
(i |^ n) div i = (i |^ n) / i