let n, k be Nat; :: thesis: ( n >= k implies n choose k >= (((n + 1) - k) |^ k) / (k !) )
set n1 = n + 1;
defpred S₁[ Nat] means ( $1 <= n implies n choose $1 >= (((n + 1) - $1) |^ $1) / ($1 !) );
( (n + 1) |^ 0 = 1 & n choose 0 = 1 & 0 ! = 1 ) by NEWTON:4, NEWTON:12, NEWTON:19;
then A1: S₁[ 0 ] ;
A2: for i being Nat st S₁[i] holds
S₁[i + 1]

proof

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
set i1 = i + 1;
assume A3: ( S₁[i] & i + 1 <= n ) ; :: thesis: n choose (i + 1) >= (((n + 1) - (i + 1)) |^ (i + 1)) / ((i + 1) !)
then A4: i < n by NAT_1:13;
A5: 0 < n - i by XREAL_1:50, A4;
(n - i) + 1 > n - i by XREAL_1:29;
then ((n + 1) - i) |^ i >= (n - i) |^ i by A5, PREPOWER:9;
then (((n + 1) - i) |^ i) / (i !) >= ((n - i) |^ i) / (i !) by XREAL_1:72;
then n choose i >= ((n - i) |^ i) / (i !) by A3, NAT_1:13, XXREAL_0:2;
then A6: ((n - i) / (i + 1)) * (n choose i) >= ((n - i) / (i + 1)) * (((n - i) |^ i) / (i !)) by XREAL_1:64, A5;
((n - i) / (i + 1)) * (((n - i) |^ i) / (i !)) = ((n - i) * ((n - i) |^ i)) / ((i + 1) * (i !)) by XCMPLX_1:76
.= ((n - i) |^ (i + 1)) / ((i + 1) * (i !)) by NEWTON:6
.= ((n - i) |^ (i + 1)) / ((i + 1) !) by NEWTON:15 ;
hence n choose (i + 1) >= (((n + 1) - (i + 1)) |^ (i + 1)) / ((i + 1) !) by A6, IRRAT_1:5; :: thesis: verum

end;

for i being Nat holds S₁[i] from NAT_1:sch 2(A1, A2);
hence ( n >= k implies n choose k >= (((n + 1) - k) |^ k) / (k !) ) ; :: thesis: verum