let n, k be Element of NAT ; :: thesis: n choose (k + 1) = ((n - k) / (k + 1)) * (n choose k)

per cases ( k + 1 <= n or ( k + 1 > n & k <= n ) or ( k + 1 > n & k > n ) ) ;

suppose A1: k + 1 <= n ; :: thesis: n choose (k + 1) = ((n - k) / (k + 1)) * (n choose k)

then reconsider l = n - (k + 1) as Element of NAT by INT_1:18;
l + 1 = n - k ;
then reconsider l1 = n - k as Element of NAT ;
k <= k + 1 by NAT_1:11;
then A2: k <= n by A1, XXREAL_0:2;
thus n choose (k + 1) = (n ! ) / (((k + 1) ! ) * (l ! )) by A1, NEWTON:def 3
.= (n ! ) / (((k ! ) * (k + 1)) * (l ! )) by NEWTON:21
.= (n ! ) / (((k ! ) * (k + 1)) * (((l ! ) * (l + 1)) / (l + 1))) by XCMPLX_1:90
.= (n ! ) / (((k ! ) * (k + 1)) * (((l + 1) ! ) / (l + 1))) by NEWTON:21
.= (l1 / (k + 1)) * ((n ! ) / ((k ! ) * (l1 ! ))) by XCMPLX_1:235
.= ((n - k) / (k + 1)) * (n choose k) by A2, NEWTON:def 3 ; :: thesis: verum

end;

suppose A3: ( k + 1 > n & k <= n ) ; :: thesis: n choose (k + 1) = ((n - k) / (k + 1)) * (n choose k)

then ( k >= n & k <= n ) by NAT_1:13;
then k = n by XXREAL_0:1;
hence n choose (k + 1) = ((n - k) / (k + 1)) * (n choose k) by A3, NEWTON:def 3; :: thesis: verum

end;

suppose A4: ( k + 1 > n & k > n ) ; :: thesis: n choose (k + 1) = ((n - k) / (k + 1)) * (n choose k)

hence n choose (k + 1) = ((n - k) / (k + 1)) * 0 by NEWTON:def 3
.= ((n - k) / (k + 1)) * (n choose k) by A4, NEWTON:def 3 ;
:: thesis: verum

end;

end;