+theorem le_exp_Al:\forall n. O < n \to exp 2 n \le A (2 * n).
+intros.
+apply (trans_le ? ((exp 2 (2*n))/(2*n)))
+ [apply le_times_to_le_div
+ [rewrite > (times_n_O O) in ⊢ (? % ?).
+ apply lt_times
+ [apply lt_O_S
+ |assumption
+ ]
+ |simplify in ⊢ (? ? (? ? %)).
+ rewrite < plus_n_O.
+ rewrite > exp_plus_times.
+ apply le_times_l.
+ alias id "le_times_SSO_n_exp_SSO_n" = "cic:/matita/nat/o/le_times_SSO_n_exp_SSO_n.con".
+ apply le_times_SSO_n_exp_SSO_n
+ ]
+ |apply le_times_to_le_div2
+ [rewrite > (times_n_O O) in ⊢ (? % ?).
+ apply lt_times
+ [apply lt_O_S
+ |assumption
+ ]
+ |apply (trans_le ? ((B (2*n)*(2*n))))
+ [rewrite < sym_times in ⊢ (? ? %).
+ apply le_exp_B.
+ assumption
+ |apply le_times_l.
+ apply le_B_A
+ ]
+ ]
+ ]
+qed.
+
+theorem le_exp_A2:\forall n. 1 < n \to exp 2 (n / 2) \le A n.
+intros.
+apply (trans_le ? (A(n/2*2)))
+ [rewrite > sym_times.
+ apply le_exp_Al.
+ elim (le_to_or_lt_eq ? ? (le_O_n (n/2)))
+ [assumption
+ |apply False_ind.
+ apply (lt_to_not_le ? ? H).
+ rewrite > (div_mod n 2)
+ [rewrite < H1.
+ change in ⊢ (? % ?) with (n\mod 2).
+ apply le_S_S_to_le.
+ apply lt_mod_m_m.
+ apply lt_O_S
+ |apply lt_O_S
+ ]
+ ]
+ |apply monotonic_A.
+ rewrite > (div_mod n 2) in ⊢ (? ? %).
+ apply le_plus_n_r.
+ apply lt_O_S
+ ]
+qed.
+