let n, k be Nat; :: thesis: ( k <= n implies n choose k <= n |^ k )
defpred S₁[ Nat] means ( $1 <= n implies n choose $1 <= n |^ $1 );
n choose 0 = 1 by NEWTON:19;
then A1: S₁[ 0 ] by NEWTON:4;
A2: for m being Nat st S₁[m] holds
S₁[m + 1]

proof

let m be Nat; :: thesis: ( S₁[m] implies S₁[m + 1] )
assume A3: S₁[m] ; :: thesis: S₁[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 S₁[m] from NAT_1:sch 2(A1, A2);
hence ( k <= n implies n choose k <= n |^ k ) ; :: thesis: verum