theorem :: ASYMPT_1:81

for n being Element of NAT st n >= 10 holds
(2 to_power (2 * n)) / (n !) < 1 / (2 to_power (n - 9)) by Lm34;