let n, m be Nat; :: thesis: ( m >= 1 implies n + 1 <= (n + m) choose m )

defpred S_{1}[ Nat] means for n being Element of NAT st $1 >= 1 holds

n + 1 <= (n + $1) choose $1;

A1: for k being Nat st S_{1}[k] holds

S_{1}[k + 1]

reconsider m9 = m as Element of NAT by ORDINAL1:def 12;

assume A8: m >= 1 ; :: thesis: n + 1 <= (n + m) choose m

A9: S_{1}[ 0 ]
;

for k being Nat holds S_{1}[k]
from NAT_1:sch 2(A9, A1);

then n9 + 1 <= (n9 + m9) choose m9 by A8;

hence n + 1 <= (n + m) choose m ; :: thesis: verum

defpred S

n + 1 <= (n + $1) choose $1;

A1: for k being Nat st S

S

proof

reconsider n9 = n as Element of NAT by ORDINAL1:def 12;
let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

set k9 = k + 1;

reconsider k9 = k + 1 as Element of NAT ;

assume A2: S_{1}[k]
; :: thesis: S_{1}[k + 1]

for n being Element of NAT st k9 >= 1 holds

n + 1 <= (n + k9) choose k9_{1}[k + 1]
; :: thesis: verum

end;set k9 = k + 1;

reconsider k9 = k + 1 as Element of NAT ;

assume A2: S

for n being Element of NAT st k9 >= 1 holds

n + 1 <= (n + k9) choose k9

proof

hence
S
let n be Element of NAT ; :: thesis: ( k9 >= 1 implies n + 1 <= (n + k9) choose k9 )

assume A3: k9 >= 1 ; :: thesis: n + 1 <= (n + k9) choose k9

end;assume A3: k9 >= 1 ; :: thesis: n + 1 <= (n + k9) choose k9

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

end;

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

A6: (n + k9) choose k9 =
((n + k) + 1) choose (k + 1)

.= ((n + k) choose (k + 1)) + ((n + k) choose k) by NEWTON:22 ;

n + 1 <= (n + k) choose k by A2, A5;

then A7: (n + 1) + ((n + k) choose (k + 1)) <= (n + k9) choose k9 by A6, XREAL_1:6;

0 + (n + 1) <= ((n + k) choose (k + 1)) + (n + 1) by XREAL_1:6;

hence n + 1 <= (n + k9) choose k9 by A7, XXREAL_0:2; :: thesis: verum

end;.= ((n + k) choose (k + 1)) + ((n + k) choose k) by NEWTON:22 ;

n + 1 <= (n + k) choose k by A2, A5;

then A7: (n + 1) + ((n + k) choose (k + 1)) <= (n + k9) choose k9 by A6, XREAL_1:6;

0 + (n + 1) <= ((n + k) choose (k + 1)) + (n + 1) by XREAL_1:6;

hence n + 1 <= (n + k9) choose k9 by A7, XXREAL_0:2; :: thesis: verum

reconsider m9 = m as Element of NAT by ORDINAL1:def 12;

assume A8: m >= 1 ; :: thesis: n + 1 <= (n + m) choose m

A9: S

for k being Nat holds S

then n9 + 1 <= (n9 + m9) choose m9 by A8;

hence n + 1 <= (n + m) choose m ; :: thesis: verum