let m, n be natural number ; :: thesis: ( m >= 1 implies n + 1 <= (n + m) choose m )
defpred S₁[ Nat] means for n being Element of NAT st $1 >= 1 holds
n + 1 <= (n + $1) choose $1;
A1: S₁[ 0 ] ;
A2: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A3: S₁[k] ; :: thesis: S₁[k + 1]
set k' = k + 1;
reconsider k' = k + 1 as Element of NAT by ORDINAL1:def 13;
for n being Element of NAT st k' >= 1 holds
n + 1 <= (n + k') choose k'

proof

let n be Element of NAT ; :: thesis: ( k' >= 1 implies n + 1 <= (n + k') choose k' )
assume A4: k' >= 1 ; :: thesis: n + 1 <= (n + k') choose k'

per cases ( k + 1 = 1 or k >= 1 ) by A4, NAT_1:8;

suppose A5: k + 1 = 1 ; :: thesis: n + 1 <= (n + k') choose k'

n + 1 >= 0 + 1 by XREAL_1:8;
hence n + 1 <= (n + k') choose k' by A5, NEWTON:33; :: thesis: verum

end;

suppose k >= 1 ; :: thesis: n + 1 <= (n + k') choose k'

then A6: n + 1 <= (n + k) choose k by A3;
A7: (n + k') choose k' = ((n + k) + 1) choose (k + 1)
.= ((n + k) choose (k + 1)) + ((n + k) choose k) by NEWTON:32 ;
A8: (n + 1) + ((n + k) choose (k + 1)) <= (n + k') choose k' by A7, A6, XREAL_1:8;
0 + (n + 1) <= ((n + k) choose (k + 1)) + (n + 1) by XREAL_1:8;
hence n + 1 <= (n + k') choose k' by A8, XXREAL_0:2; :: thesis: verum

end;

end;

end;

hence S₁[k + 1] ; :: thesis: verum

end;

A9: for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A1, A2);
assume A10: m >= 1 ; :: thesis: n + 1 <= (n + m) choose m
reconsider m' = m as Element of NAT by ORDINAL1:def 13;
reconsider n' = n as Element of NAT by ORDINAL1:def 13;
n' + 1 <= (n' + m') choose m' by A9, A10;
hence n + 1 <= (n + m) choose m ; :: thesis: verum