let n, m be Nat; :: thesis: ( m >= 1 & n >= 1 implies m + 1 <= (n + m) choose m )
defpred S₁[ Nat] means for n being Element of NAT st $1 >= 1 & n >= 1 holds
$1 + 1 <= (n + $1) choose $1;
assume A1: ( m >= 1 & n >= 1 ) ; :: thesis: m + 1 <= (n + m) choose m
reconsider n9 = n as Element of NAT by ORDINAL1:def 12;
reconsider m9 = m as Element of NAT by ORDINAL1:def 12;
A2: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

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

proof

let n be Element of NAT ; :: thesis: ( k9 >= 1 & n >= 1 implies k9 + 1 <= (n + k9) choose k9 )
assume A4: k9 >= 1 ; :: thesis: ( not n >= 1 or k9 + 1 <= (n + k9) choose k9 )
assume A5: n >= 1 ; :: thesis: k9 + 1 <= (n + k9) choose k9

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

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

( n + 1 >= 0 + 1 & n + 1 >= 1 + 1 ) by A5, XREAL_1:6;
hence k9 + 1 <= (n + k9) choose k9 by A6, NEWTON:23; :: thesis: verum

end;

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

set k99 = k + 1;
A8: (n + k9) choose k9 = ((n + k) + 1) choose (k + 1)
.= ((n + k) choose (k + 1)) + ((n + k) choose k) by NEWTON:22 ;
k + 1 >= 0 + 1 by XREAL_1:6;
then A9: (n -' 1) + 1 <= ((n -' 1) + (k + 1)) choose (k + 1) by Th11;
n - 1 >= 1 - 1 by A5, XREAL_1:9;
then n -' 1 = n - 1 by XREAL_0:def 2;
then 1 <= (n + k) choose (k + 1) by A5, A9, XXREAL_0:2;
then A10: 1 + (k + 1) <= ((n + k) choose (k + 1)) + (k + 1) by XREAL_1:6;
(k + 1) + ((n + k) choose (k + 1)) <= (n + k9) choose k9 by A3, A5, A7, A8, XREAL_1:6;
hence k9 + 1 <= (n + k9) choose k9 by A10, XXREAL_0:2; :: thesis: verum

end;

end;

end;

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

end;

A11: S₁[ 0 ] ;
for k being Nat holds S₁[k] from NAT_1:sch 2(A11, A2);
then m9 + 1 <= (n9 + m9) choose m9 by A1;
hence m + 1 <= (n + m) choose m ; :: thesis: verum