let i, n be Nat; :: thesis: ( n > 0 implies (i |^ n) div i = (i |^ n) / i )
assume n > 0 ; :: thesis: (i |^ n) div i = (i |^ n) / i
then (i |^ n) mod i = 0 by Th36;
hence (i |^ n) div i = (i |^ n) / i by Th63; :: thesis: verum