+ |apply le_S.apply le_n
+ ]
+ ]
+ ]
+ ]
+ ]
+qed.
+
+theorem le_A_exp2: \forall n. O < n \to
+A(n) \le (exp (S(S O)) ((S(S O)) * (S(S O)) * n)).
+intros.
+apply (trans_le ? (A (exp (S(S O)) (S(log (S(S O)) n)))))
+ [apply monotonic_A.
+ apply lt_to_le.
+ apply lt_exp_log.
+ apply le_n
+ |apply (trans_le ? ((exp (S(S O)) ((S(S O))*(exp (S(S O)) (S(log (S(S O)) n)))))))
+ [apply le_A_exp1
+ |apply le_exp
+ [apply lt_O_S
+ |rewrite > assoc_times.apply le_times_r.
+ change with ((S(S O))*((S(S O))\sup(log (S(S O)) n))≤(S(S O))*n).
+ apply le_times_r.
+ apply le_exp_log.
+ assumption
+ ]
+ ]
+ ]
+qed.
+
+(* example *)
+theorem A_SO: A (S O) = S O.
+reflexivity.
+qed.
+
+theorem A_SSO: A (S(S O)) = S (S O).
+reflexivity.
+qed.
+
+theorem A_SSSO: A (S(S(S O))) = S(S(S(S(S(S O))))).
+reflexivity.
+qed.
+
+theorem A_SSSSO: A (S(S(S(S O)))) = S(S(S(S(S(S(S(S(S(S(S(S O))))))))))).
+reflexivity.
+qed.
+
+(* da spostare *)
+theorem or_eq_eq_S: \forall n.\exists m.
+n = (S(S O))*m \lor n = S ((S(S O))*m).
+intro.elim n
+ [apply (ex_intro ? ? O).
+ left.reflexivity
+ |elim H.elim H1
+ [apply (ex_intro ? ? a).
+ right.apply eq_f.assumption
+ |apply (ex_intro ? ? (S a)).
+ left.rewrite > H2.
+ apply sym_eq.
+ apply times_SSO
+ ]
+ ]
+qed.
+
+theorem times_exp:
+\forall n,m,p. exp n p * exp m p = exp (n*m) p.
+intros.elim p
+ [simplify.reflexivity
+ |simplify.
+ rewrite > assoc_times.
+ rewrite < assoc_times in ⊢ (? ? (? ? %) ?).
+ rewrite < sym_times in ⊢ (? ? (? ? (? % ?)) ?).
+ rewrite > assoc_times in ⊢ (? ? (? ? %) ?).
+ rewrite < assoc_times.
+ rewrite < H.
+ reflexivity
+ ]
+qed.
+
+theorem monotonic_exp1: \forall n.
+monotonic nat le (\lambda x.(exp x n)).
+unfold monotonic. intros.
+simplify.elim n
+ [apply le_n
+ |simplify.
+ apply le_times;assumption
+ ]
+qed.
+
+(* a better result *)
+theorem le_A_exp3: \forall n. S O < n \to
+A(n) \le exp (pred n) (S(S O))*(exp (S(S O)) ((S(S O)) * n)).
+intro.
+apply (nat_elim1 n).
+intros.
+elim (or_eq_eq_S m).
+elim H2
+ [elim (le_to_or_lt_eq (S O) a)
+ [rewrite > H3 in ⊢ (? % ?).
+ apply (trans_le ? ((exp (S(S O)) ((S(S O)*a)))*A a))
+ [apply le_A_exp
+ |apply (trans_le ? (((S(S O)))\sup((S(S O))*a)*
+ ((pred a)\sup((S(S O)))*((S(S O)))\sup((S(S O))*a))))
+ [apply le_times_r.
+ apply H
+ [rewrite > H3.
+ rewrite > times_n_SO in ⊢ (? % ?).
+ rewrite > sym_times.
+ apply lt_times_l1
+ [apply lt_to_le.assumption
+ |apply le_n
+ ]
+ |assumption
+ ]
+ |rewrite > sym_times.
+ rewrite > assoc_times.
+ rewrite < exp_plus_times.
+ apply (trans_le ?
+ (pred a\sup((S(S O)))*(S(S O))\sup(S(S O))*(S(S O))\sup((S(S O))*m)))
+ [rewrite > assoc_times.
+ apply le_times_r.
+ rewrite < exp_plus_times.
+ apply le_exp
+ [apply lt_O_S
+ |rewrite < H3.
+ simplify.
+ rewrite < plus_n_O.
+ apply le_S.apply le_S.
+ apply le_n
+ ]
+ |apply le_times_l.
+ rewrite > times_exp.
+ apply monotonic_exp1.
+ rewrite > H3.
+ rewrite > sym_times.
+ cases a
+ [apply le_n
+ |simplify.
+ rewrite < plus_n_Sm.
+ apply le_S.
+ apply le_n
+ ]