let i, j, n be Nat; :: thesis: ( i <= j & 2 * j <= n + 1 implies n choose i <= n choose j )
defpred S₁[ Nat] means ( i <= $1 & 2 * $1 <= n + 1 implies n choose i <= n choose $1 );
A1: S₁[ 0 ] ;
A2: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
set k1 = k + 1;
assume A3: ( S₁[k] & i <= k + 1 & 2 * (k + 1) <= n + 1 ) ; :: thesis: n choose i <= n choose (k + 1)

per cases then ( i = k + 1 or i < k + 1 ) by XXREAL_0:1;

suppose i = k + 1 ; :: thesis: n choose i <= n choose (k + 1)

hence n choose i <= n choose (k + 1) ; :: thesis: verum

end;

suppose A4: i < k + 1 ; :: thesis: n choose i <= n choose (k + 1)

k < k + 1 by NAT_1:13;
then A5: 2 * k <= 2 * (k + 1) by XREAL_1:66;
(k + 1) + (k + 1) <= n + 1 by A3;
then k + 1 <= (n + 1) - (k + 1) by XREAL_1:19;
then (n - k) / (k + 1) >= 1 by XREAL_1:181;
then ((n - k) / (k + 1)) * (n choose k) >= 1 * (n choose k) by XREAL_1:66;
then n choose (k + 1) >= n choose k by IRRAT_1:5;
hence n choose i <= n choose (k + 1) by A5, A4, NAT_1:13, A3, XXREAL_0:2; :: thesis: verum

end;

end;

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A1, A2);
hence ( i <= j & 2 * j <= n + 1 implies n choose i <= n choose j ) ; :: thesis: verum