let s, t be natural Number ; :: 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:5;
A2: s + 1 <= t by A1, NAT_1:13;
then reconsider m2 = t - (s + 1) as Element of NAT by INT_1:5;
A3: s + 1 <= t + 1 by A1, XREAL_1:6;
then reconsider m = (t + 1) - (s + 1) as Element of NAT by INT_1:5;
t choose (s + 1) = (t !) / (((s + 1) !) * (m2 !)) by A2, Def3;
then A4: (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:116
.= (((t !) * ((s !) * (m1 !))) + ((t !) * (((s !) * (s + 1)) * (m2 !)))) / ((((s + 1) !) * (m2 !)) * ((s !) * (m1 !))) by Th15
.= ((s !) * ((t !) * ((m1 !) + ((s + 1) * (m2 !))))) / ((s !) * ((m1 !) * (((s + 1) !) * (m2 !))))
.= ((t !) * (((m2 + 1) !) + ((s + 1) * (m2 !)))) / ((m1 !) * (((s + 1) !) * (m2 !))) by XCMPLX_1:91
.= ((t !) * (((m2 !) * (m2 + 1)) + ((m2 !) * (s + 1)))) / ((m1 !) * (((s + 1) !) * (m2 !))) by Th15
.= ((m2 !) * ((t !) * ((m2 + 1) + (s + 1)))) / ((m2 !) * (((s + 1) !) * (m1 !)))
.= ((t !) * (t - (s - (s + 1)))) / (((s + 1) !) * (m1 !)) by XCMPLX_1:91
.= ((t + 1) !) / (((s + 1) !) * (m1 !)) by Th15 ;
m = m1 ;
hence (t + 1) choose (s + 1) = (t choose (s + 1)) + (t choose s) by A4, A3, Def3; :: thesis: verum

end;

end;

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

then s < t + 1 by NAT_1:13;
then A6: t choose (s + 1) = 0 by A5, Def3;
(t + 1) choose (s + 1) = 1 by A5, Th21;
hence (t + 1) choose (s + 1) = (t choose (s + 1)) + (t choose s) by A5, A6, Th21; :: thesis: verum

end;

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

then s + 1 > t + 1 by XREAL_1:8;
then A8: (t + 1) choose (s + 1) = 0 by Def3;
A9: s + 1 > t + 0 by A7, XREAL_1:8;
t choose s = 0 by A7, Def3;
hence (t + 1) choose (s + 1) = (t choose (s + 1)) + (t choose s) by A9, A8, Def3; :: thesis: verum

end;

end;