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