let n, k be Nat; :: thesis: ( k <= n implies n ! <= (k !) * (n |^ (n -' k)) )
assume A1: k <= n ; :: thesis: n ! <= (k !) * (n |^ (n -' k))
then reconsider nk = n - k as Nat by NAT_1:21;
defpred S₁[ Nat] means (k + $1) ! <= (k !) * ((k + $1) |^ $1);
(k + 0) |^ 0 = 1 by NEWTON:4;
then A2: S₁[ 0 ] ;
A3: for i being Nat st S₁[i] holds
S₁[i + 1]

proof

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
set ki1 = (k + i) + 1;
assume A4: S₁[i] ; :: thesis: S₁[i + 1]
A5: ( (k + i) |^ 0 = 1 & ((k + i) + 1) |^ 0 = 1 ) by NEWTON:4;
A6: (((k + i) + 1) |^ i) * ((k + i) + 1) = ((k + i) + 1) |^ (i + 1) by NEWTON:6;
( k + i < (k + i) + 1 & ( i >= 1 or i = 0 ) ) by NAT_1:13, NAT_1:14;
then (k + i) |^ i <= ((k + i) + 1) |^ i by A5, PREPOWER:10;
then (k !) * ((k + i) |^ i) <= (k !) * (((k + i) + 1) |^ i) by XREAL_1:66;
then A7: (k + i) ! <= (k !) * (((k + i) + 1) |^ i) by A4, XXREAL_0:2;
((k + i) + 1) ! = ((k + i) !) * ((k + i) + 1) by NEWTON:15;
then ((k + i) + 1) ! <= ((k !) * (((k + i) + 1) |^ i)) * ((k + i) + 1) by A7, XREAL_1:66;
hence S₁[i + 1] by A6; :: thesis: verum

end;

for i being Nat holds S₁[i] from NAT_1:sch 2(A2, A3);
then S₁[nk] ;
hence n ! <= (k !) * (n |^ (n -' k)) by A1, XREAL_1:233; :: thesis: verum