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 12;
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 6;
then - [\(n / 2)/] >= - (n / 2) by XREAL_1:24;
then A5: (- [\(n / 2)/]) + (n + 1) >= (- (n / 2)) + (n + 1) by XREAL_1:6;
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:53;
2 * n >= 1 * n by XREAL_1:64;
then A7: ( n / 2 >= [\(n / 2)/] & (2 * n) / 2 >= n / 2 ) by INT_1:def 6, XREAL_1:72;
then A8: n >= m by XXREAL_0:2;
n - m = n -' m by A7, XREAL_1:233, XXREAL_0:2;
then reconsider l = n - [\(n / 2)/] as Element of NAT ;
((n + 1) !) / (n !) = ((n + 1) * (n !)) / (n !) by NEWTON:15
.= (n + 1) * ((n !) / (n !)) by XCMPLX_1:74
.= (n + 1) * 1 by XCMPLX_1:60 ;
then A9: (n !) / ((n + 1) !) = 1 / (n + 1) by XCMPLX_1:57;
A10: (- (n / 2)) + (n + 1) = (n / 2) + 1 ;
set nk = n - k;
set l1 = (n + 1) -' m1;
A11: 1 * m1 <= 2 * m1 by XREAL_1:64;
assume A12: m1 = [\((n + 1) / 2)/] ; :: thesis: (n + 1) choose m1 >= (n + 1) choose k
then m1 <= (n + 1) / 2 by INT_1:def 6;
then A13: m1 * 2 <= ((n + 1) / 2) * 2 by XREAL_1:64;
then A14: ( n + 1 >= m1 & (n + 1) -' m1 = (n + 1) - m1 ) by A11, XREAL_1:233, XXREAL_0:2;
A15: (n + 1) / 2 >= [\((n + 1) / 2)/] by INT_1:def 6;
A16: n >= k

proof

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

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

hence n >= k by A1, A6, A12, INT_1:def 6; :: thesis: verum

end;

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

then n + 1 > 0 + 1 by XREAL_1:6;
then n >= 1 by NAT_1:13;
then n + n >= 1 + n by XREAL_1:6;
then (2 * n) / 2 >= (n + 1) / 2 by XREAL_1:72;
then n >= [\((n + 1) / 2)/] by A15, XXREAL_0:2;
hence n >= k by A6, A12, XXREAL_0:2; :: thesis: verum

end;

end;

end;

then n - k = n -' k by XREAL_1:233;
then reconsider nk = n - k as Element of NAT ;
(n / 2) - 1 < [\(n / 2)/] by INT_1:def 6;
then A17: ((n / 2) - 1) + 1 < [\(n / 2)/] + 1 by XREAL_1:6;
(n + 1) - k = nk + 1 ;
then reconsider nk1 = (n + 1) - k as Element of NAT ;
0 + n <= 1 + n by XREAL_1:6;
then A18: k <= n + 1 by A16, XXREAL_0:2;
then A19: (n + 1) choose k = ((n + 1) !) / ((nk1 !) * (k !)) by NEWTON:def 3;
A20: (nk1 !) / (nk !) = ((nk + 1) * (nk !)) / (nk !) by NEWTON:15
.= (nk + 1) * ((nk !) / (nk !)) by XCMPLX_1:74
.= (nk + 1) * 1 by XCMPLX_1:60 ;
n choose k = (n !) / ((nk !) * (k !)) by A16, NEWTON:def 3;
then (n choose k) / ((n + 1) choose k) = ((n !) / ((nk !) * (k !))) / (((n + 1) !) / ((nk1 !) * (k !))) by A18, NEWTON:def 3
.= (((n !) / ((nk !) * (k !))) / ((n + 1) !)) * ((nk1 !) * (k !)) by XCMPLX_1:82
.= ((n !) / (((n + 1) !) * ((nk !) * (k !)))) * ((nk1 !) * (k !)) by XCMPLX_1:78
.= ((1 / (n + 1)) / ((nk !) * (k !))) * ((nk1 !) * (k !)) by A9, XCMPLX_1:78
.= (1 / (n + 1)) / (((nk !) * (k !)) / ((nk1 !) * (k !))) by XCMPLX_1:82
.= (1 / (n + 1)) / (((nk !) / (nk1 !)) / ((k !) / (k !))) by XCMPLX_1:84
.= (1 / (n + 1)) / (((nk !) / (nk1 !)) / 1) by XCMPLX_1:60
.= (1 / (n + 1)) / (1 / (nk + 1)) by A20, XCMPLX_1:57
.= (1 * (nk + 1)) / (1 * (n + 1)) by XCMPLX_1:84
.= (nk + 1) / (n + 1) ;
then A21: (n choose k) / (((n + 1) choose k) / ((n + 1) choose k)) = ((nk + 1) / (n + 1)) * ((n + 1) choose k) by XCMPLX_1:82;
A22: n choose k = (n choose k) / 1
.= ((nk + 1) / (n + 1)) * ((n + 1) choose k) by A19, A21, XCMPLX_1:60 ;
then A23: (n choose k) * ((n + 1) / (l + 1)) = ((((nk + 1) / (n + 1)) * ((n + 1) choose k)) * (n + 1)) / (l + 1) by XCMPLX_1:74
.= ((((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:75
.= ((1 * (nk + 1)) * ((n + 1) choose k)) / (l + 1) by XCMPLX_1:60
.= ((n + 1) choose k) * ((nk + 1) / (l + 1)) by XCMPLX_1:74 ;
A24: (n choose k) * ((n + 1) / (m + 1)) = ((((nk + 1) / (n + 1)) * ((n + 1) choose k)) * (n + 1)) / (m + 1) by A22, XCMPLX_1:74
.= ((((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:75
.= ((1 * (nk + 1)) * ((n + 1) choose k)) / (m + 1) by XCMPLX_1:60
.= ((n + 1) choose k) * ((nk + 1) / (m + 1)) by XCMPLX_1:74 ;

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
A25: n = 2 * k1 by A4, ABIAN:def 2;
A26: [\((n + 1) / 2)/] = [\(((2 * k1) / 2) + (1 / 2))/] by A25
.= k1 + [\(1 / 2)/] by INT_1:28
.= k1 + 0 by A1, INT_1:def 6
.= [\(n / 2)/] by A25, INT_1:25 ;
then A27: n choose m >= n choose k by A3, A6, A12;
- k >= - [\(n / 2)/] by A6, A12, A26, XREAL_1:24;
then (- k) + (n + 1) >= (- [\(n / 2)/]) + (n + 1) by XREAL_1:6;
then ((n - k) + 1) / ((n - [\(n / 2)/]) + 1) >= ((n - [\(n / 2)/]) + 1) / ((n - [\(n / 2)/]) + 1) by A5, A10, XREAL_1:72;
then ((n - k) + 1) / ((n - [\(n / 2)/]) + 1) >= 1 by A5, A10, XCMPLX_1:60;
then A28: (((n - k) + 1) / ((n - [\(n / 2)/]) + 1)) * ((n + 1) choose k) >= 1 * ((n + 1) choose k) by XREAL_1:64;
A29: (n + 1) -' m1 = (n + 1) - m1 by A13, A11, XREAL_1:233, XXREAL_0:2
.= l + 1 by A12, A26 ;
(n + 1) choose m1 = ((n + 1) !) / ((m1 !) * (((n + 1) -' m1) !)) by A14, NEWTON:def 3
.= ((n + 1) * (n !)) / ((m !) * ((l + 1) !)) by A12, A26, A29, NEWTON:15
.= ((n + 1) * (n !)) / ((m !) * ((l + 1) * (l !))) by NEWTON:15
.= ((n + 1) * (n !)) / ((l + 1) * ((m !) * (l !)))
.= ((n + 1) / (l + 1)) / (((m !) * (l !)) / (n !)) by XCMPLX_1:84
.= ((n !) / ((m !) * (l !))) * ((n + 1) / (l + 1)) by XCMPLX_1:80
.= (n choose m) * ((n + 1) / (l + 1)) by A8, NEWTON:def 3 ;
then (n + 1) choose m >= ((n + 1) choose k) * ((nk + 1) / (l + 1)) by A12, A23, A26, A27, XREAL_1:64;
hence (n + 1) choose m1 >= (n + 1) choose k by A12, A26, A28, 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
A30: n = (2 * j) + 1 by ABIAN:1;
A31: [\((n + 1) / 2)/] = (j + 0) + 1 by A30, INT_1:25
.= (j + [\(1 / 2)/]) + 1 by A1, INT_1:def 6
.= [\(j + (1 / 2))/] + 1 by INT_1:28
.= [\(n / 2)/] + 1 by A30 ;
A32: (n + 1) -' m1 = (n + 1) - m1 by A13, A11, XREAL_1:233, XXREAL_0:2
.= l by A12, A31 ;

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

end;

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

then A33: k <= m by NAT_1:13;
then A34: n choose m >= n choose k by A3;
n / 2 >= [\(n / 2)/] by INT_1:def 6;
then (n / 2) * 2 >= [\(n / 2)/] * 2 by XREAL_1:64;
then n - [\(n / 2)/] >= ([\(n / 2)/] * 2) - [\(n / 2)/] by XREAL_1:9;
then n - [\(n / 2)/] >= k by A33, XXREAL_0:2;
then (n - [\(n / 2)/]) - (k - [\(n / 2)/]) >= k - (k - [\(n / 2)/]) by XREAL_1:9;
then (n - k) + 1 >= [\(n / 2)/] + 1 by XREAL_1:6;
then ((n - k) + 1) / ([\(n / 2)/] + 1) >= ([\(n / 2)/] + 1) / ([\(n / 2)/] + 1) by A17, XREAL_1:72;
then ((n - k) + 1) / ([\(n / 2)/] + 1) >= 1 by A17, XCMPLX_1:60;
then A35: (((n - k) + 1) / ([\(n / 2)/] + 1)) * ((n + 1) choose k) >= 1 * ((n + 1) choose k) by XREAL_1:64;
(n + 1) choose m1 = ((n + 1) !) / ((m1 !) * (((n + 1) -' m1) !)) by A14, NEWTON:def 3
.= ((n + 1) * (n !)) / (((m + 1) !) * (l !)) by A12, A31, A32, NEWTON:15
.= ((n + 1) * (n !)) / (((m !) * (m + 1)) * (l !)) by NEWTON:15
.= ((n + 1) * (n !)) / ((m + 1) * ((m !) * (l !)))
.= ((n + 1) / (m + 1)) / (((m !) * (l !)) / (n !)) by XCMPLX_1:84
.= ((n !) / ((m !) * (l !))) * ((n + 1) / (m + 1)) by XCMPLX_1:80
.= (n choose m) * ((n + 1) / (m + 1)) by A8, NEWTON:def 3 ;
then (n + 1) choose m1 >= ((n + 1) choose k) * ((nk + 1) / (m + 1)) by A24, A34, XREAL_1:64;
hence (n + 1) choose m1 >= (n + 1) choose k by A35, XXREAL_0:2; :: thesis: verum

end;

end;

end;

end;

end;

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

end;

A36: S₁[ 0 ]

proof

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

end;

A38: for n being Nat holds S₁[n] from NAT_1:sch 2(A36, 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 )
A39: n in NAT by ORDINAL1:def 12;
assume A40: k <= n ; :: thesis: ( not m = [\(n / 2)/] or n choose m >= n choose k )
assume A41: 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 A38, A41; :: thesis: verum

end;

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

set r = n -' k;
A43: n -' k = n - k by A40, XREAL_1:233;
then A44: n choose k = n choose (n -' k) by A40, NEWTON:20;

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

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

- k < - m by A42, XREAL_1:24;
then A46: (- k) + n < (- m) + n by XREAL_1:6;
ex j being Element of NAT st n = 2 * j by A39, A45, ABIAN:def 2;
then n / 2 = [\(n / 2)/] by INT_1:25;
hence n choose m >= n choose k by A38, A41, A43, A44, A46; :: thesis: verum

end;

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

then consider j being Integer such that
A47: n = (2 * j) + 1 by ABIAN:1;
A48: k >= m + 1 by A42, NAT_1:13;
A49: [\(n / 2)/] = [\(j + (1 / 2))/] by A47
.= j + [\(1 / 2)/] by INT_1:28
.= j + 0 by A1, INT_1:def 6
.= j ;

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

suppose A50: 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:64;
then A51: ( n / 2 >= [\(n / 2)/] & (2 * n) / 2 >= n / 2 ) by INT_1:def 6, XREAL_1:72;
then A52: n >= m by A41, XXREAL_0:2;
n - m = n -' m by A41, A51, XREAL_1:233, XXREAL_0:2;
then reconsider nm = n - m as Element of NAT ;
2 * m >= 1 * m by XREAL_1:64;
then A53: n >= m + 1 by A41, A47, A49, XREAL_1:6;
then n - (m + 1) = n -' (m + 1) by XREAL_1:233;
then reconsider nm1 = n - (m + 1) as Element of NAT ;
A54: n choose (m + 1) = (n !) / ((nm1 !) * ((m + 1) !)) by A53, NEWTON:def 3;
nm = m + 1 by A41, A47, A49;
hence n choose m >= n choose k by A50, A52, A54, NEWTON:def 3; :: thesis: verum

end;

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

then - k < - (m + 1) by XREAL_1:24;
then (- k) + n < (- (m + 1)) + n by XREAL_1:6;
hence n choose m >= n choose k by A38, A41, A43, A44, A47, A49; :: 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