A1: ( 0 <= 1 / 2 & (1 / 2) - 1 < 0 ) ;
defpred S₁[ Nat] means for k, m being Nat st k <= m & m = [\($1 / 2)/] holds
$1 choose m >= $1 choose k;
A2: S₁[ 0 ]

proof

let k, m be Nat; :: thesis: ( k <= m & m = [\(0 / 2)/] implies 0 choose m >= 0 choose k )
assume A3: k <= m ; :: thesis: ( not m = [\(0 / 2)/] or 0 choose m >= 0 choose k )
assume m = [\(0 / 2)/] ; :: thesis: 0 choose m >= 0 choose k
then m = 0 by INT_1:47;
hence 0 choose m >= 0 choose k by A3; :: thesis: verum

end;

A5: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
A6: n in NAT by ORDINAL1:def 13;
assume A7: S₁[n] ; :: thesis: S₁[n + 1]
for k, m1 being Nat st k <= m1 & m1 = [\((n + 1) / 2)/] holds
(n + 1) choose m1 >= (n + 1) choose k

proof

let k, m1 be Nat; :: thesis: ( k <= m1 & m1 = [\((n + 1) / 2)/] implies (n + 1) choose m1 >= (n + 1) choose k )
assume A8: k <= m1 ; :: thesis: ( not m1 = [\((n + 1) / 2)/] or (n + 1) choose m1 >= (n + 1) choose k )
assume A9: m1 = [\((n + 1) / 2)/] ; :: thesis: (n + 1) choose m1 >= (n + 1) choose k
then ( m1 <= (n + 1) / 2 & ((n + 1) / 2) - 1 < m1 ) by INT_1:def 4;
then A10: m1 * 2 <= ((n + 1) / 2) * 2 by XREAL_1:66;
A11: 1 * m1 <= 2 * m1 by XREAL_1:66;
then A12: n + 1 >= m1 by A10, XXREAL_0:2;
set l1 = (n + 1) -' m1;
A13: (n + 1) -' m1 = (n + 1) - m1 by A10, A11, XREAL_1:235, XXREAL_0:2;
set m = [\(n / 2)/];
set l = n - [\(n / 2)/];
reconsider m = [\(n / 2)/] as Element of NAT by INT_1:80;
A14: n / 2 >= [\(n / 2)/] by INT_1:def 4;
A15: (n + 1) / 2 >= [\((n + 1) / 2)/] by INT_1:def 4;
2 * n >= 1 * n by XREAL_1:66;
then A16: (2 * n) / 2 >= n / 2 by XREAL_1:74;
then A17: n >= m by A14, XXREAL_0:2;
n - m = n -' m by A14, A16, XREAL_1:235, XXREAL_0:2;
then reconsider l = n - [\(n / 2)/] as Element of NAT ;
A18: n >= k

proof

per cases ( n = 0 or n <> 0 ) ;

suppose n = 0 ; :: thesis: n >= k

hence n >= k by A1, A8, A9, INT_1:def 4; :: thesis: verum

end;

suppose n <> 0 ; :: thesis: n >= k

then n + 1 > 0 + 1 by XREAL_1:8;
then n >= 1 by NAT_1:13;
then n + n >= 1 + n by XREAL_1:8;
then (2 * n) / 2 >= (n + 1) / 2 by XREAL_1:74;
then n >= [\((n + 1) / 2)/] by A15, XXREAL_0:2;
hence n >= k by A8, A9, XXREAL_0:2; :: thesis: verum

end;

end;

end;

set nk = n - k;
n - k = n -' k by A18, XREAL_1:235;
then reconsider nk = n - k as Element of NAT ;
set nk1 = (n + 1) - k;
(n + 1) - k = nk + 1 ;
then reconsider nk1 = (n + 1) - k as Element of NAT ;
A19: n ! <> 0 by NEWTON:23;
((n + 1) ! ) / (n ! ) = ((n + 1) * (n ! )) / (n ! ) by NEWTON:21
.= (n + 1) * ((n ! ) / (n ! )) by XCMPLX_1:75
.= (n + 1) * 1 by A19, XCMPLX_1:60 ;
then A20: (n ! ) / ((n + 1) ! ) = 1 / (n + 1) by XCMPLX_1:57;
A21: k ! <> 0 by NEWTON:23;
A22: nk ! <> 0 by NEWTON:23;
A23: (nk1 ! ) / (nk ! ) = ((nk + 1) * (nk ! )) / (nk ! ) by NEWTON:21
.= (nk + 1) * ((nk ! ) / (nk ! )) by XCMPLX_1:75
.= (nk + 1) * 1 by A22, XCMPLX_1:60 ;
A24: n choose k = (n ! ) / ((nk ! ) * (k ! )) by A18, NEWTON:def 3;
0 + n <= 1 + n by XREAL_1:8;
then A25: k <= n + 1 by A18, XXREAL_0:2;
then A26: (n + 1) choose k = ((n + 1) ! ) / ((nk1 ! ) * (k ! )) by NEWTON:def 3;
A27: (n choose k) / ((n + 1) choose k) = ((n ! ) / ((nk ! ) * (k ! ))) / (((n + 1) ! ) / ((nk1 ! ) * (k ! ))) by A24, A25, NEWTON:def 3
.= (((n ! ) / ((nk ! ) * (k ! ))) / ((n + 1) ! )) * ((nk1 ! ) * (k ! )) by XCMPLX_1:83
.= ((n ! ) / (((n + 1) ! ) * ((nk ! ) * (k ! )))) * ((nk1 ! ) * (k ! )) by XCMPLX_1:79
.= ((1 / (n + 1)) / ((nk ! ) * (k ! ))) * ((nk1 ! ) * (k ! )) by A20, XCMPLX_1:79
.= (1 / (n + 1)) / (((nk ! ) * (k ! )) / ((nk1 ! ) * (k ! ))) by XCMPLX_1:83
.= (1 / (n + 1)) / (((nk ! ) / (nk1 ! )) / ((k ! ) / (k ! ))) by XCMPLX_1:85
.= (1 / (n + 1)) / (((nk ! ) / (nk1 ! )) / 1) by A21, XCMPLX_1:60
.= (1 / (n + 1)) / (1 / (nk + 1)) by A23, XCMPLX_1:57
.= (1 * (nk + 1)) / (1 * (n + 1)) by XCMPLX_1:85
.= (nk + 1) / (n + 1) ;
A28: (nk1 ! ) * (k ! ) <> 0 by NEWTON:25;
A29: (n + 1) ! <> 0 by NEWTON:23;
A30: (n choose k) / (((n + 1) choose k) / ((n + 1) choose k)) = ((nk + 1) / (n + 1)) * ((n + 1) choose k) by A27, XCMPLX_1:83;
A31: n choose k = (n choose k) / 1
.= ((nk + 1) / (n + 1)) * ((n + 1) choose k) by A26, A28, A29, A30, XCMPLX_1:60 ;
[\(n / 2)/] <= n / 2 by INT_1:def 4;
then - [\(n / 2)/] >= - (n / 2) by XREAL_1:26;
then A32: (- [\(n / 2)/]) + (n + 1) >= (- (n / 2)) + (n + 1) by XREAL_1:8;
A33: (- (n / 2)) + (n + 1) = (n / 2) + 1 ;
(n / 2) - 1 < [\(n / 2)/] by INT_1:def 4;
then A34: ((n / 2) - 1) + 1 < [\(n / 2)/] + 1 by XREAL_1:8;
A35: (n choose k) * ((n + 1) / (l + 1)) = ((((nk + 1) / (n + 1)) * ((n + 1) choose k)) * (n + 1)) / (l + 1) by A31, XCMPLX_1:75
.= ((((nk + 1) / (n + 1)) * (n + 1)) * ((n + 1) choose k)) / (l + 1)
.= ((((n + 1) / (n + 1)) * (nk + 1)) * ((n + 1) choose k)) / (l + 1) by XCMPLX_1:76
.= ((1 * (nk + 1)) * ((n + 1) choose k)) / (l + 1) by XCMPLX_1:60
.= ((n + 1) choose k) * ((nk + 1) / (l + 1)) by XCMPLX_1:75 ;
A36: (n choose k) * ((n + 1) / (m + 1)) = ((((nk + 1) / (n + 1)) * ((n + 1) choose k)) * (n + 1)) / (m + 1) by A31, XCMPLX_1:75
.= ((((nk + 1) / (n + 1)) * (n + 1)) * ((n + 1) choose k)) / (m + 1)
.= ((((n + 1) / (n + 1)) * (nk + 1)) * ((n + 1) choose k)) / (m + 1) by XCMPLX_1:76
.= ((1 * (nk + 1)) * ((n + 1) choose k)) / (m + 1) by XCMPLX_1:60
.= ((n + 1) choose k) * ((nk + 1) / (m + 1)) by XCMPLX_1:75 ;

per cases ( n is even or not n is even ) ;

suppose n is even ; :: thesis: (n + 1) choose m1 >= (n + 1) choose k

then consider k1 being Element of NAT such that
A37: n = 2 * k1 by A6, ABIAN:def 2;
A38: [\((n + 1) / 2)/] = [\(((2 * k1) / 2) + (1 / 2))/] by A37
.= k1 + [\(1 / 2)/] by INT_1:51
.= k1 + 0 by A1, INT_1:def 4
.= [\(n / 2)/] by A37, INT_1:47 ;
A39: (n + 1) -' m1 = (n + 1) - m1 by A10, A11, XREAL_1:235, XXREAL_0:2
.= l + 1 by A9, A38 ;
A40: n choose m >= n choose k by A7, A8, A9, A38;
(n + 1) choose m1 = ((n + 1) ! ) / ((m1 ! ) * (((n + 1) -' m1) ! )) by A12, A13, NEWTON:def 3
.= ((n + 1) * (n ! )) / ((m ! ) * ((l + 1) ! )) by A9, A38, A39, NEWTON:21
.= ((n + 1) * (n ! )) / ((m ! ) * ((l + 1) * (l ! ))) by NEWTON:21
.= ((n + 1) * (n ! )) / ((l + 1) * ((m ! ) * (l ! )))
.= ((n + 1) / (l + 1)) / (((m ! ) * (l ! )) / (n ! )) by XCMPLX_1:85
.= ((n ! ) / ((m ! ) * (l ! ))) * ((n + 1) / (l + 1)) by XCMPLX_1:81
.= (n choose m) * ((n + 1) / (l + 1)) by A17, NEWTON:def 3 ;
then A41: (n + 1) choose m >= ((n + 1) choose k) * ((nk + 1) / (l + 1)) by A9, A35, A38, A40, XREAL_1:66;
- k >= - [\(n / 2)/] by A8, A9, A38, XREAL_1:26;
then (- k) + (n + 1) >= (- [\(n / 2)/]) + (n + 1) by XREAL_1:8;
then ((n - k) + 1) / ((n - [\(n / 2)/]) + 1) >= ((n - [\(n / 2)/]) + 1) / ((n - [\(n / 2)/]) + 1) by A32, A33, XREAL_1:74;
then ((n - k) + 1) / ((n - [\(n / 2)/]) + 1) >= 1 by A32, A33, XCMPLX_1:60;
then (((n - k) + 1) / ((n - [\(n / 2)/]) + 1)) * ((n + 1) choose k) >= 1 * ((n + 1) choose k) by XREAL_1:66;
hence (n + 1) choose m1 >= (n + 1) choose k by A9, A38, A41, XXREAL_0:2; :: thesis: verum

end;

suppose not n is even ; :: thesis: (n + 1) choose m1 >= (n + 1) choose k

then consider j being Integer such that
A42: n = (2 * j) + 1 by ABIAN:1;
A43: [\((n + 1) / 2)/] = (j + 0 ) + 1 by A42, INT_1:47
.= (j + [\(1 / 2)/]) + 1 by A1, INT_1:def 4
.= [\(j + (1 / 2))/] + 1 by INT_1:51
.= [\(n / 2)/] + 1 by A42 ;
A44: (n + 1) -' m1 = (n + 1) - m1 by A10, A11, XREAL_1:235, XXREAL_0:2
.= l by A9, A43 ;

per cases ( k = m + 1 or k < m + 1 ) by A8, A9, A43, XXREAL_0:1;

suppose k = m + 1 ; :: thesis: (n + 1) choose m1 >= (n + 1) choose k

hence (n + 1) choose m1 >= (n + 1) choose k by A9, A43; :: thesis: verum

end;

suppose k < m + 1 ; :: thesis: (n + 1) choose m1 >= (n + 1) choose k

then A45: k <= m by NAT_1:13;
then A46: n choose m >= n choose k by A7;
(n + 1) choose m1 = ((n + 1) ! ) / ((m1 ! ) * (((n + 1) -' m1) ! )) by A12, A13, NEWTON:def 3
.= ((n + 1) * (n ! )) / (((m + 1) ! ) * (l ! )) by A9, A43, A44, NEWTON:21
.= ((n + 1) * (n ! )) / (((m ! ) * (m + 1)) * (l ! )) by NEWTON:21
.= ((n + 1) * (n ! )) / ((m + 1) * ((m ! ) * (l ! )))
.= ((n + 1) / (m + 1)) / (((m ! ) * (l ! )) / (n ! )) by XCMPLX_1:85
.= ((n ! ) / ((m ! ) * (l ! ))) * ((n + 1) / (m + 1)) by XCMPLX_1:81
.= (n choose m) * ((n + 1) / (m + 1)) by A17, NEWTON:def 3 ;
then A47: (n + 1) choose m1 >= ((n + 1) choose k) * ((nk + 1) / (m + 1)) by A36, A46, XREAL_1:66;
n / 2 >= [\(n / 2)/] by INT_1:def 4;
then (n / 2) * 2 >= [\(n / 2)/] * 2 by XREAL_1:66;
then n - [\(n / 2)/] >= ([\(n / 2)/] * 2) - [\(n / 2)/] by XREAL_1:11;
then n - [\(n / 2)/] >= k by A45, XXREAL_0:2;
then (n - [\(n / 2)/]) - (k - [\(n / 2)/]) >= k - (k - [\(n / 2)/]) by XREAL_1:11;
then (n - k) + 1 >= [\(n / 2)/] + 1 by XREAL_1:8;
then ((n - k) + 1) / ([\(n / 2)/] + 1) >= ([\(n / 2)/] + 1) / ([\(n / 2)/] + 1) by A34, XREAL_1:74;
then ((n - k) + 1) / ([\(n / 2)/] + 1) >= 1 by A34, XCMPLX_1:60;
then (((n - k) + 1) / ([\(n / 2)/] + 1)) * ((n + 1) choose k) >= 1 * ((n + 1) choose k) by XREAL_1:66;
hence (n + 1) choose m1 >= (n + 1) choose k by A47, XXREAL_0:2; :: thesis: verum

end;

end;

end;

end;

end;

hence S₁[n + 1] ; :: thesis: verum

end;

A48: for n being Nat holds S₁[n] from NAT_1:sch 2(A2, A5);
for n, k, m being Nat st k <= n & m = [\(n / 2)/] holds
n choose m >= n choose k

proof

let n, k, m be Nat; :: thesis: ( k <= n & m = [\(n / 2)/] implies n choose m >= n choose k )
A49: n in NAT by ORDINAL1:def 13;
assume A50: k <= n ; :: thesis: ( not m = [\(n / 2)/] or n choose m >= n choose k )
assume A51: m = [\(n / 2)/] ; :: thesis: n choose m >= n choose k

per cases ( k <= m or k > m ) ;

suppose k <= m ; :: thesis: n choose m >= n choose k

hence n choose m >= n choose k by A48, A51; :: thesis: verum

end;

suppose A52: k > m ; :: thesis: n choose m >= n choose k

set r = n -' k;
A53: n -' k = n - k by A50, XREAL_1:235;
then A54: n choose k = n choose (n -' k) by A50, NEWTON:30;

per cases ( n is even or not n is even ) ;

suppose n is even ; :: thesis: n choose m >= n choose k

then consider j being Element of NAT such that
A55: n = 2 * j by A49, ABIAN:def 2;
A56: n / 2 = [\(n / 2)/] by A55, INT_1:47;
- k < - m by A52, XREAL_1:26;
then (- k) + n < (- m) + n by XREAL_1:8;
hence n choose m >= n choose k by A48, A51, A53, A54, A56; :: thesis: verum

end;

suppose not n is even ; :: thesis: n choose m >= n choose k

then consider j being Integer such that
A57: n = (2 * j) + 1 by ABIAN:1;
A58: [\(n / 2)/] = [\(j + (1 / 2))/] by A57
.= j + [\(1 / 2)/] by INT_1:51
.= j + 0 by A1, INT_1:def 4
.= j ;
A59: k >= m + 1 by A52, NAT_1:13;

per cases ( k = m + 1 or k > m + 1 ) by A59, XXREAL_0:1;

suppose A60: k = m + 1 ; :: thesis: n choose m >= n choose k

A61: n / 2 >= [\(n / 2)/] by INT_1:def 4;
2 * m >= 1 * m by XREAL_1:66;
then A62: n >= m + 1 by A51, A57, A58, XREAL_1:8;
2 * n >= 1 * n by XREAL_1:66;
then A63: (2 * n) / 2 >= n / 2 by XREAL_1:74;
then A64: n >= m by A51, A61, XXREAL_0:2;
set nm = n - m;
n - m = n -' m by A51, A61, A63, XREAL_1:235, XXREAL_0:2;
then reconsider nm = n - m as Element of NAT ;
set nm1 = n - (m + 1);
n - (m + 1) = n -' (m + 1) by A62, XREAL_1:235;
then reconsider nm1 = n - (m + 1) as Element of NAT ;
A65: n choose (m + 1) = (n ! ) / ((nm1 ! ) * ((m + 1) ! )) by A62, NEWTON:def 3;
nm = m + 1 by A51, A57, A58;
hence n choose m >= n choose k by A60, A64, A65, NEWTON:def 3; :: thesis: verum

end;

suppose k > m + 1 ; :: thesis: n choose m >= n choose k

then - k < - (m + 1) by XREAL_1:26;
then (- k) + n < (- (m + 1)) + n by XREAL_1:8;
hence n choose m >= n choose k by A48, A51, A53, A54, A57, A58; :: thesis: verum

end;

end;

end;

end;

end;

end;

end;

hence for n, k, m being Nat st k <= n & m = [\(n / 2)/] holds
n choose m >= n choose k ; :: thesis: verum