let k, n be Element of 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:18;
set l1 = l + 1;
A2:
l + 1 = (n + 1) - k
;
0 + 1 <= l + 1
by XREAL_1:8;
then
1 / 1 >= 1 / (l + 1)
by XREAL_1:87;
then A3:
(n choose k) * (1 / 1) >= (n choose k) * (1 / (l + 1))
by XREAL_1:66;
n + 0 <= n + 1
by XREAL_1:8;
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:21
.=
(((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:21
.=
((n ! ) * 1) / (((k ! ) * (l ! )) * (l + 1))
.=
((n ! ) / ((k ! ) * (l ! ))) * (1 / (l + 1))
by XCMPLX_1:77
.=
(n choose k) * (1 / (l + 1))
by A1, NEWTON:def 3
;
hence
n choose k >= ((n + 1) choose k) / (n + 1)
by A3; verum