let n, k be Nat; :: thesis: ( n >= k implies n choose k <= (n |^ k) / (k !) )
defpred S₁[ Nat] means ( $1 <= n implies n choose $1 <= (n |^ $1) / ($1 !) );
( n |^ 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 |^ (i + 1)) / ((i + 1) !)
then A4: i < n by NAT_1:13;
A5: 0 < n - i by XREAL_1:50, A4;
n - i <= n - 0 by XREAL_1:10;
then (n - i) / (i + 1) <= n / (i + 1) by XREAL_1:72;
then A6: ((n - i) / (i + 1)) * (n choose i) <= (n / (i + 1)) * ((n |^ i) / (i !)) by A5, NAT_1:13, A3, XREAL_1:66;
(n / (i + 1)) * ((n |^ i) / (i !)) = (n * (n |^ i)) / ((i + 1) * (i !)) by XCMPLX_1:76
.= (n |^ (i + 1)) / ((i + 1) * (i !)) by NEWTON:6
.= (n |^ (i + 1)) / ((i + 1) !) by NEWTON:15 ;
hence n choose (i + 1) <= (n |^ (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 |^ k) / (k !) ) ; :: thesis: verum