let i, n be Nat; :: 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, Th36;
hence (i |^ n) div i = (i |^ n) / i by A2, Th63; :: 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;