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:61
.= 2 * 2 by RVSUM_1:99
.= 4 ;
reconsider m = [\((2 * n) / 2)/] as Element of NAT by ORDINAL1:def 12;
2 * n >= 2 * 1 by A1, NAT_1:14, XREAL_1:64;
then (2 * n) choose m >= (2 |^ (2 * n)) / (2 * n) by Th5;
hence (2 * n) choose n >= (4 |^ n) / (2 * n) by A2, NEWTON:9; :: thesis: verum

end;

end;