let n, k be Nat; :: thesis: ( n <> 0 & 1 <= k implies (n |^ k) div n = n |^ (k -' 1) )
assume A1: ( n <> 0 & 1 <= k ) ; :: thesis: (n |^ k) div n = n |^ (k -' 1)
then A2: k - 1 >= 1 - 1 by XREAL_1:11;
k = (k - 1) + 1
.= (k -' 1) + 1 by A2, XREAL_0:def 2 ;
then n |^ k = n * (n |^ (k -' 1)) by NEWTON:11;
hence (n |^ k) div n = n |^ (k -' 1) by A1, NAT_D:18; :: thesis: verum