let n, m be Nat; :: thesis: ( m >= 1 implies n + 1 <= (n + m) choose m )
defpred S1[ Nat] means for n being Element of NAT st \$1 >= 1 holds
n + 1 <= (n + \$1) choose \$1;
A1: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
set k9 = k + 1;
reconsider k9 = k + 1 as Element of NAT ;
assume A2: S1[k] ; :: thesis: S1[k + 1]
for n being Element of NAT st k9 >= 1 holds
n + 1 <= (n + k9) choose k9
proof
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
per cases ( k + 1 = 1 or k >= 1 ) by ;
suppose A4: k + 1 = 1 ; :: thesis: n + 1 <= (n + k9) choose k9
n + 1 >= 0 + 1 by XREAL_1:6;
hence n + 1 <= (n + k9) choose k9 by ; :: thesis: verum
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 ;
0 + (n + 1) <= ((n + k) choose (k + 1)) + (n + 1) by XREAL_1:6;
hence n + 1 <= (n + k9) choose k9 by ; :: thesis: verum
end;
end;
end;
hence S1[k + 1] ; :: thesis: verum
end;
reconsider n9 = n as Element of NAT by ORDINAL1:def 12;
reconsider m9 = m as Element of NAT by ORDINAL1:def 12;
assume A8: m >= 1 ; :: thesis: n + 1 <= (n + m) choose m
A9: S1[ 0 ] ;
for k being Nat holds S1[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