let n, k be Nat; :: thesis: ( k <= n implies n choose k <= n |^ k )
defpred S1[ Nat] means ( $1 <= n implies n choose $1 <= n |^ $1 );
n choose 0 = 1 by NEWTON:19;
then A1: S1[ 0 ] by NEWTON:4;
A2: for m being Nat st S1[m] holds
S1[m + 1]
proof
let m be Nat; :: thesis: ( S1[m] implies S1[m + 1] )
assume A3: S1[m] ; :: thesis: S1[m + 1]
set m1 = m + 1;
assume A4: m + 1 <= n ; :: thesis: n choose (m + 1) <= n |^ (m + 1)
then m < n by NAT_1:13;
then A5: n - m > m - m by XREAL_1:14;
A6: n - m <= n - 0 by XREAL_1:10;
A7: n choose (m + 1) = ((n - m) / (m + 1)) * (n choose m) by IRRAT_1:5;
(n - m) / (m + 1) <= (n - m) / 1 by A5, XREAL_1:118, NAT_1:11;
then (n - m) / (m + 1) <= n by A6, XXREAL_0:2;
then A8: n choose (m + 1) <= n * (n choose m) by A7, XREAL_1:64;
n * (n choose m) <= n * (n |^ m) by A3, A4, NAT_1:13, XREAL_1:64;
then n choose (m + 1) <= n * (n |^ m) by A8, XXREAL_0:2;
hence n choose (m + 1) <= n |^ (m + 1) by NEWTON:6; :: thesis: verum
end;
for m being Nat holds S1[m] from NAT_1:sch 2(A1, A2);
 hence ( k <= n implies n choose k <= n |^ k ) ; :: thesis: verum