+theorem le_n_SSSSSSSSO_to_le_A_exp:
+\forall n. n \le 8 \to A(n) \le exp 2 ((2 * n) -3).
+intro.cases n
+ [intro.apply le_n
+ |cases n1
+ [intro.apply le_n
+ |cases n2
+ [intro.apply le_n
+ |cases n3
+ [intro.apply leb_true_to_le.reflexivity
+ |cases n4
+ [intro.apply leb_true_to_le.reflexivity
+ |cases n5
+ [intro.apply leb_true_to_le.reflexivity
+ |cases n6
+ [intro.apply leb_true_to_le.reflexivity
+ |cases n7
+ [intro.apply leb_true_to_le.reflexivity
+ |cases n8
+ [intro.apply leb_true_to_le.reflexivity
+ |intro.apply False_ind.
+ apply (lt_to_not_le ? ? H).
+ apply leb_true_to_le.reflexivity
+ ]
+ ]
+ ]
+ ]
+ ]
+ ]
+ ]
+ ]
+ ]
+qed.
+
+theorem le_A_exp5: \forall n. A(n) \le exp 2 ((2 * n) -3).
+intro.
+apply (nat_elim1 n).
+intros.
+elim (decidable_le 9 m)
+ [elim (or_eq_eq_S m).
+ elim H2
+ [rewrite > H3 in ⊢ (? % ?).
+ apply (trans_le ? (exp 2 (pred(2*a))*A a))
+ [apply le_A_exp
+ |apply (trans_le ? (2\sup(pred(2*a))*(2\sup((2*a)-3))))
+ [apply le_times_r.
+ apply H.
+ rewrite > H3.
+ apply lt_m_nm
+ [apply (trans_lt ? 4)
+ [apply lt_O_S
+ |apply (lt_times_to_lt 2)
+ [apply lt_O_S
+ |rewrite < H3.assumption
+ ]
+ ]
+ |apply le_n
+ ]
+ |rewrite < H3.
+ rewrite < exp_plus_times.
+ apply le_exp
+ [apply lt_O_S
+ |simplify.rewrite < plus_n_O.
+ rewrite > eq_minus_plus_plus_minus
+ [apply le_plus_l.
+ apply le_pred_n
+ |apply (trans_le ? 9)
+ [apply leb_true_to_le. reflexivity
+ |assumption
+ ]
+ ]
+ ]
+ ]
+ ]
+ |apply (trans_le ? (A (2*(S a))))
+ [apply monotonic_A.
+ rewrite > H3.
+ rewrite > times_SSO.
+ apply le_n_Sn
+ |apply (trans_le ? ((exp 2 ((2*(S a))-2))*A (S a)))
+ [apply lt_SSSSO_to_le_A_exp.
+ apply le_S_S.
+ apply (le_times_to_le 2)
+ [apply le_n_Sn.
+ |apply le_S_S_to_le.rewrite < H3.assumption
+ ]
+ |apply (trans_le ? ((2\sup((2*S a)-2))*(exp 2 ((2*(S a))-3))))
+ [apply le_times_r.
+ apply H.
+ rewrite > H3.
+ apply le_S_S.
+ apply lt_m_nm
+ [apply (lt_to_le_to_lt ? 4)
+ [apply lt_O_S
+ |apply (le_times_to_le 2)
+ [apply lt_O_S
+ |apply le_S_S_to_le.
+ rewrite < H3.assumption
+ ]
+ ]
+ |apply le_n
+ ]
+ |rewrite > times_SSO.
+ rewrite < H3.
+ rewrite < exp_plus_times.
+ apply le_exp
+ [apply lt_O_S
+ |cases m
+ [apply le_n
+ |cases n1
+ [apply le_n
+ |simplify.
+ rewrite < minus_n_O.
+ rewrite < plus_n_O.
+ rewrite < plus_n_Sm.
+ simplify.rewrite < minus_n_O.
+ rewrite < plus_n_Sm.
+ apply le_n
+ ]
+ ]
+ ]
+ ]
+ ]
+ ]
+ ]
+ |apply le_n_SSSSSSSSO_to_le_A_exp.
+ apply le_S_S_to_le.
+ apply not_le_to_lt.
+ assumption
+ ]
+qed.
+
+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.
+ 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.
+