let t, s be Nat; :: thesis: (t + 1) choose (s + 1) = (t choose (s + 1)) + (t choose s)

per cases ( s < t or s = t or s > t ) by XXREAL_0:1;

suppose A1: s < t ; :: thesis: (t + 1) choose (s + 1) = (t choose (s + 1)) + (t choose s)

thus (t + 1) choose (s + 1) = (t choose (s + 1)) + (t choose s) :: thesis: verum

proof

reconsider m1 = t - s as Element of NAT by A1, INT_1:18;
A2: s + 1 <= t by A1, NAT_1:13;
then reconsider m2 = t - (s + 1) as Element of NAT by INT_1:18;
A3: t choose (s + 1) = (t ! ) / (((s + 1) ! ) * (m2 ! )) by A2, Def3;
A4: ( ((s + 1) ! ) * (m2 ! ) <> 0 & (s ! ) * (m1 ! ) <> 0 ) by Th25;
A5: s ! <> 0 by Th23;
A6: m2 ! <> 0 by Th23;
A7: (t choose (s + 1)) + (t choose s) = ((t ! ) / (((s + 1) ! ) * (m2 ! ))) + ((t ! ) / ((s ! ) * (m1 ! ))) by A1, A3, Def3
.= (((t ! ) * ((s ! ) * (m1 ! ))) + ((t ! ) * (((s + 1) ! ) * (m2 ! )))) / ((((s + 1) ! ) * (m2 ! )) * ((s ! ) * (m1 ! ))) by A4, XCMPLX_1:117
.= (((t ! ) * ((s ! ) * (m1 ! ))) + ((t ! ) * (((s ! ) * (s + 1)) * (m2 ! )))) / ((((s + 1) ! ) * (m2 ! )) * ((s ! ) * (m1 ! ))) by Th21
.= ((s ! ) * ((t ! ) * ((m1 ! ) + ((s + 1) * (m2 ! ))))) / ((s ! ) * ((m1 ! ) * (((s + 1) ! ) * (m2 ! ))))
.= ((t ! ) * (((m2 + 1) ! ) + ((s + 1) * (m2 ! )))) / ((m1 ! ) * (((s + 1) ! ) * (m2 ! ))) by A5, XCMPLX_1:92
.= ((t ! ) * (((m2 ! ) * (m2 + 1)) + ((m2 ! ) * (s + 1)))) / ((m1 ! ) * (((s + 1) ! ) * (m2 ! ))) by Th21
.= ((m2 ! ) * ((t ! ) * ((m2 + 1) + (s + 1)))) / ((m2 ! ) * (((s + 1) ! ) * (m1 ! )))
.= ((t ! ) * (t - (s - (s + 1)))) / (((s + 1) ! ) * (m1 ! )) by A6, XCMPLX_1:92
.= ((t + 1) ! ) / (((s + 1) ! ) * (m1 ! )) by Th21 ;
A8: s + 1 <= t + 1 by A1, XREAL_1:8;
then reconsider m = (t + 1) - (s + 1) as Element of NAT by INT_1:18;
m = m1 ;
hence (t + 1) choose (s + 1) = (t choose (s + 1)) + (t choose s) by A7, A8, Def3; :: thesis: verum

end;

end;

suppose A9: s = t ; :: thesis: (t + 1) choose (s + 1) = (t choose (s + 1)) + (t choose s)

then s < t + 1 by NAT_1:13;
then ( (t + 1) choose (s + 1) = 1 & t choose s = 1 & t choose (s + 1) = 0 ) by A9, Def3, Th31;
hence (t + 1) choose (s + 1) = (t choose (s + 1)) + (t choose s) ; :: thesis: verum

end;

suppose A10: s > t ; :: thesis: (t + 1) choose (s + 1) = (t choose (s + 1)) + (t choose s)

then ( s + 1 > t + 0 & s + 1 > t + 1 ) by XREAL_1:10;
then ( (t + 1) choose (s + 1) = 0 & t choose s = 0 & t choose (s + 1) = 0 ) by A10, Def3;
hence (t + 1) choose (s + 1) = (t choose (s + 1)) + (t choose s) ; :: thesis: verum

end;

end;