let k, n be 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:5;
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:15
.= (n !) / (((k !) * (k + 1)) * (((l !) * (l + 1)) / (l + 1))) by XCMPLX_1:89
.= (n !) / (((k !) * (k + 1)) * (((l + 1) !) / (l + 1))) by NEWTON:15
.= (l1 / (k + 1)) * ((n !) / ((k !) * (l1 !))) by XCMPLX_1:233
.= ((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 by NAT_1:13;
then k = n by A3, 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;