let k, n be Nat; ( k <= n implies n choose k >= ((n + 1) choose k) / (n + 1) )
set n1 = n + 1;
assume A1:
k <= n
; n choose k >= ((n + 1) choose k) / (n + 1)
then reconsider l = n - k as Element of NAT by INT_1:5;
set l1 = l + 1;
A2:
l + 1 = (n + 1) - k
;
0 + 1 <= l + 1
by XREAL_1:6;
then
1 / 1 >= 1 / (l + 1)
by XREAL_1:85;
then A3:
(n choose k) * (1 / 1) >= (n choose k) * (1 / (l + 1))
by XREAL_1:64;
n + 0 <= n + 1
by XREAL_1:6;
then
k <= n + 1
by A1, XXREAL_0:2;
then ((n + 1) choose k) / (n + 1) =
(((n + 1) !) / ((k !) * ((l + 1) !))) / (n + 1)
by A2, NEWTON:def 3
.=
(((n + 1) * (n !)) / ((k !) * ((l + 1) !))) / ((n + 1) * 1)
by NEWTON:15
.=
(((n + 1) * (n !)) * (((k !) * ((l + 1) !)) ")) / ((n + 1) * 1)
.=
((n + 1) * ((n !) * (((k !) * ((l + 1) !)) "))) / ((n + 1) * 1)
.=
((n + 1) * ((n !) / ((k !) * ((l + 1) !)))) / ((n + 1) * 1)
.=
((n + 1) / (n + 1)) * (((n !) / ((k !) * ((l + 1) !))) / 1)
.=
1 * (((n !) / ((k !) * ((l + 1) !))) / 1)
by XCMPLX_1:60
.=
(n !) / ((k !) * ((l !) * (l + 1)))
by NEWTON:15
.=
((n !) * 1) / (((k !) * (l !)) * (l + 1))
.=
((n !) / ((k !) * (l !))) * (1 / (l + 1))
by XCMPLX_1:76
.=
(n choose k) * (1 / (l + 1))
by A1, NEWTON:def 3
;
hence
n choose k >= ((n + 1) choose k) / (n + 1)
by A3; verum