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;
A3: s + 1 <= t by A1, NAT_1:13;
then reconsider m2 = t - (s + 1) as Element of NAT by INT_1:18;
A5: s + 1 <= t + 1 by A1, XREAL_1:8;
then reconsider m = (t + 1) - (s + 1) as Element of NAT by INT_1:18;
t choose (s + 1) = (t ! ) / (((s + 1) ! ) * (m2 ! )) by A3, Def3;
then A8: (t choose (s + 1)) + (t choose s) = ((t ! ) / (((s + 1) ! ) * (m2 ! ))) + ((t ! ) / ((s ! ) * (m1 ! ))) by A1, Def3
.= (((t ! ) * ((s ! ) * (m1 ! ))) + ((t ! ) * (((s + 1) ! ) * (m2 ! )))) / ((((s + 1) ! ) * (m2 ! )) * ((s ! ) * (m1 ! ))) by 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 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 XCMPLX_1:92
.= ((t + 1) ! ) / (((s + 1) ! ) * (m1 ! )) by Th21 ;
m = m1 ;
hence (t + 1) choose (s + 1) = (t choose (s + 1)) + (t choose s) by A8, A5, 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 A10: t choose (s + 1) = 0 by A9, Def3;
(t + 1) choose (s + 1) = 1 by A9, Th31;
hence (t + 1) choose (s + 1) = (t choose (s + 1)) + (t choose s) by A9, A10, Th31; :: thesis: verum

end;

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

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

end;

end;