let n be Nat; :: thesis: (2 * n) choose n >= (4 |^ n) / (2 * n)

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

suppose n = 0 ; :: thesis: (2 * n) choose n >= (4 |^ n) / (2 * n)

hence (2 * n) choose n >= (4 |^ n) / (2 * n) ; :: thesis: verum

end;

suppose A1: n <> 0 ; :: thesis: (2 * n) choose n >= (4 |^ n) / (2 * n)

set m = [\((2 * n) / 2)/];
A2: 2 |^ 2 = Product <*2,2*> by FINSEQ_2:75
.= 2 * 2 by RVSUM_1:129
.= 4 ;
A3: [\((2 * n) / 2)/] = n by INT_1:47;
then reconsider m = [\((2 * n) / 2)/] as Element of NAT by ORDINAL1:def 13;
2 * n >= 2 * 1 by A1, NAT_1:14, XREAL_1:66;
then (2 * n) choose m >= (2 |^ (2 * n)) / (2 * n) by Th5;
hence (2 * n) choose n >= (4 |^ n) / (2 * n) by A2, A3, NEWTON:14; :: thesis: verum

end;

end;