let i, n be natural number ; :: thesis: ( n > 0 implies (i |^ n) div i = (i |^ n) / i )
assume A1: n > 0 ; :: thesis: (i |^ n) div i = (i |^ n) / i

per cases ( i > 0 or i = 0 ) ;

suppose A2: i > 0 ; :: thesis: (i |^ n) div i = (i |^ n) / i

(i |^ n) mod i = 0 by A1, Th37;
hence (i |^ n) div i = (i |^ n) / i by A2, Th68; :: thesis: verum

end;

suppose A3: i = 0 ; :: thesis: (i |^ n) div i = (i |^ n) / i

n >= 0 + 1 by A1, NAT_1:13;
then i |^ n = 0 by A3, NEWTON:11;
hence (i |^ n) div i = (i |^ n) / i by A3, NAT_D:def 1; :: thesis: verum

end;

end;