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

proof

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

proof

[\(n / 2)/] <= n / 2 by INT_1:def 4;
then - [\(n / 2)/] >= - (n / 2) by XREAL_1:26;
then A5: (- [\(n / 2)/]) + (n + 1) >= (- (n / 2)) + (n + 1) by XREAL_1:8;
set m = [\(n / 2)/];
let k, m1 be Nat; :: thesis: ( k <= m1 & m1 = [\((n + 1) / 2)/] implies (n + 1) choose m1 >= (n + 1) choose k )
assume A6: k <= m1 ; :: thesis: ( not m1 = [\((n + 1) / 2)/] or (n + 1) choose m1 >= (n + 1) choose k )
set nk1 = (n + 1) - k;
set l = n - [\(n / 2)/];
reconsider m = [\(n / 2)/] as Element of NAT by INT_1:80;
A7: k ! <> 0 by NEWTON:23;
2 * n >= 1 * n by XREAL_1:66;
then A8: ( n / 2 >= [\(n / 2)/] & (2 * n) / 2 >= n / 2 ) by INT_1:def 4, XREAL_1:74;
then A9: n >= m by XXREAL_0:2;
n - m = n -' m by A8, XREAL_1:235, XXREAL_0:2;
then reconsider l = n - [\(n / 2)/] as Element of NAT ;
A10: 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 A10, XCMPLX_1:60 ;
then A11: (n ! ) / ((n + 1) ! ) = 1 / (n + 1) by XCMPLX_1:57;
A12: (- (n / 2)) + (n + 1) = (n / 2) + 1 ;
set nk = n - k;
set l1 = (n + 1) -' m1;
A13: 1 * m1 <= 2 * m1 by XREAL_1:66;
assume A14: m1 = [\((n + 1) / 2)/] ; :: thesis: (n + 1) choose m1 >= (n + 1) choose k
then m1 <= (n + 1) / 2 by INT_1:def 4;
then A15: m1 * 2 <= ((n + 1) / 2) * 2 by XREAL_1:66;
then A16: ( n + 1 >= m1 & (n + 1) -' m1 = (n + 1) - m1 ) by A13, XREAL_1:235, XXREAL_0:2;
A17: (n + 1) / 2 >= [\((n + 1) / 2)/] by INT_1:def 4;
A18: n >= k

proof

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

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

hence n >= k by A1, A6, A14, 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 A17, XXREAL_0:2;
hence n >= k by A6, A14, XXREAL_0:2; :: thesis: verum

end;

end;

end;

then n - k = n -' k by XREAL_1:235;
then reconsider nk = n - k as Element of NAT ;
A19: nk ! <> 0 by NEWTON:23;
(n / 2) - 1 < [\(n / 2)/] by INT_1:def 4;
then A20: ((n / 2) - 1) + 1 < [\(n / 2)/] + 1 by XREAL_1:8;
(n + 1) - k = nk + 1 ;
then reconsider nk1 = (n + 1) - k as Element of NAT by ORDINAL1:def 13;
0 + n <= 1 + n by XREAL_1:8;
then A21: k <= n + 1 by A18, XXREAL_0:2;
then A22: (n + 1) choose k = ((n + 1) ! ) / ((nk1 ! ) * (k ! )) by NEWTON:def 3;
A23: (nk1 ! ) / (nk ! ) = ((nk + 1) * (nk ! )) / (nk ! ) by NEWTON:21
.= (nk + 1) * ((nk ! ) / (nk ! )) by XCMPLX_1:75
.= (nk + 1) * 1 by A19, XCMPLX_1:60 ;
n choose k = (n ! ) / ((nk ! ) * (k ! )) by A18, NEWTON:def 3;
then (n choose k) / ((n + 1) choose k) = ((n ! ) / ((nk ! ) * (k ! ))) / (((n + 1) ! ) / ((nk1 ! ) * (k ! ))) by A21, 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 A11, 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 A7, 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) ;
then A24: (n choose k) / (((n + 1) choose k) / ((n + 1) choose k)) = ((nk + 1) / (n + 1)) * ((n + 1) choose k) by XCMPLX_1:83;
A25: ( (nk1 ! ) * (k ! ) <> 0 & (n + 1) ! <> 0 ) by NEWTON:23, NEWTON:25;
A26: n choose k = (n choose k) / 1
.= ((nk + 1) / (n + 1)) * ((n + 1) choose k) by A22, A25, A24, XCMPLX_1:60 ;
then A27: (n choose k) * ((n + 1) / (l + 1)) = ((((nk + 1) / (n + 1)) * ((n + 1) choose k)) * (n + 1)) / (l + 1) by 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 ;
A28: (n choose k) * ((n + 1) / (m + 1)) = ((((nk + 1) / (n + 1)) * ((n + 1) choose k)) * (n + 1)) / (m + 1) by A26, 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
A29: n = 2 * k1 by A4, ABIAN:def 2;
A30: [\((n + 1) / 2)/] = [\(((2 * k1) / 2) + (1 / 2))/] by A29
.= k1 + [\(1 / 2)/] by INT_1:51
.= k1 + 0 by A1, INT_1:def 4
.= [\(n / 2)/] by A29, INT_1:47 ;
then A31: n choose m >= n choose k by A3, A6, A14;
- k >= - [\(n / 2)/] by A6, A14, A30, 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 A5, A12, XREAL_1:74;
then ((n - k) + 1) / ((n - [\(n / 2)/]) + 1) >= 1 by A5, A12, XCMPLX_1:60;
then A32: (((n - k) + 1) / ((n - [\(n / 2)/]) + 1)) * ((n + 1) choose k) >= 1 * ((n + 1) choose k) by XREAL_1:66;
A33: (n + 1) -' m1 = (n + 1) - m1 by A15, A13, XREAL_1:235, XXREAL_0:2
.= l + 1 by A14, A30 ;
(n + 1) choose m1 = ((n + 1) ! ) / ((m1 ! ) * (((n + 1) -' m1) ! )) by A16, NEWTON:def 3
.= ((n + 1) * (n ! )) / ((m ! ) * ((l + 1) ! )) by A14, A30, A33, 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 A9, NEWTON:def 3 ;
then (n + 1) choose m >= ((n + 1) choose k) * ((nk + 1) / (l + 1)) by A14, A27, A30, A31, XREAL_1:66;
hence (n + 1) choose m1 >= (n + 1) choose k by A14, A30, A32, 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
A34: n = (2 * j) + 1 by ABIAN:1;
A35: [\((n + 1) / 2)/] = (j + 0 ) + 1 by A34, 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 A34 ;
A36: (n + 1) -' m1 = (n + 1) - m1 by A15, A13, XREAL_1:235, XXREAL_0:2
.= l by A14, A35 ;

per cases ( k = m + 1 or k < m + 1 ) by A6, A14, A35, 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 A14, A35; :: thesis: verum

end;

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

then A37: k <= m by NAT_1:13;
then A38: n choose m >= n choose k by A3;
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 A37, 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 A20, XREAL_1:74;
then ((n - k) + 1) / ([\(n / 2)/] + 1) >= 1 by A20, XCMPLX_1:60;
then A39: (((n - k) + 1) / ([\(n / 2)/] + 1)) * ((n + 1) choose k) >= 1 * ((n + 1) choose k) by XREAL_1:66;
(n + 1) choose m1 = ((n + 1) ! ) / ((m1 ! ) * (((n + 1) -' m1) ! )) by A16, NEWTON:def 3
.= ((n + 1) * (n ! )) / (((m + 1) ! ) * (l ! )) by A14, A35, A36, 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 A9, NEWTON:def 3 ;
then (n + 1) choose m1 >= ((n + 1) choose k) * ((nk + 1) / (m + 1)) by A28, A38, XREAL_1:66;
hence (n + 1) choose m1 >= (n + 1) choose k by A39, XXREAL_0:2; :: thesis: verum

end;

end;

end;

end;

end;

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

end;

A40: S₁[ 0 ]

proof

let k, m be Nat; :: thesis: ( k <= m & m = [\(0 / 2)/] implies 0 choose m >= 0 choose k )
assume A41: 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 A41; :: thesis: verum

end;

A42: for n being Nat holds S₁[n] from NAT_1:sch 2(A40, A2);
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 )
A43: n in NAT by ORDINAL1:def 13;
assume A44: k <= n ; :: thesis: ( not m = [\(n / 2)/] or n choose m >= n choose k )
assume A45: 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 A42, A45; :: thesis: verum

end;

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

set r = n -' k;
A47: n -' k = n - k by A44, XREAL_1:235;
then A48: n choose k = n choose (n -' k) by A44, NEWTON:30;

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

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

- k < - m by A46, XREAL_1:26;
then A50: (- k) + n < (- m) + n by XREAL_1:8;
ex j being Element of NAT st n = 2 * j by A43, A49, ABIAN:def 2;
then n / 2 = [\(n / 2)/] by INT_1:47;
hence n choose m >= n choose k by A42, A45, A47, A48, A50; :: thesis: verum

end;

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

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

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

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

set nm1 = n - (m + 1);
set nm = n - m;
2 * n >= 1 * n by XREAL_1:66;
then A55: ( n / 2 >= [\(n / 2)/] & (2 * n) / 2 >= n / 2 ) by INT_1:def 4, XREAL_1:74;
then A56: n >= m by A45, XXREAL_0:2;
n - m = n -' m by A45, A55, XREAL_1:235, XXREAL_0:2;
then reconsider nm = n - m as Element of NAT ;
2 * m >= 1 * m by XREAL_1:66;
then A57: n >= m + 1 by A45, A51, A53, XREAL_1:8;
then n - (m + 1) = n -' (m + 1) by XREAL_1:235;
then reconsider nm1 = n - (m + 1) as Element of NAT ;
A58: n choose (m + 1) = (n ! ) / ((nm1 ! ) * ((m + 1) ! )) by A57, NEWTON:def 3;
nm = m + 1 by A45, A51, A53;
hence n choose m >= n choose k by A54, A56, A58, 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 A42, A45, A47, A48, A51, A53; :: 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