+
+theorem exp_n_O: \forall n. O < n \to exp O n = O.
+intros.apply (lt_O_n_elim ? H).intros.
+simplify.reflexivity.
+qed.
+
+(*
+theorem tech1: \forall n,i.O < n \to
+(exp (S n) (S(S i)))/(exp n (S i)) \le ((exp n i) + (exp (S n) (S i)))/(exp n i).
+intros.
+simplify in ⊢ (? (? ? %) ?).
+rewrite < eq_div_div_div_times
+ [apply monotonic_div
+ [apply lt_O_exp.assumption
+ |apply le_S_S_to_le.
+ apply lt_times_to_lt_div.
+ change in ⊢ (? % ?) with ((exp (S n) (S i)) + n*(exp (S n) (S i))).
+
+
+ |apply (trans_le ? ((n)\sup(i)*(S n)\sup(S i)/(n)\sup(S i)))
+ [apply le_times_div_div_times.
+ apply lt_O_exp.assumption
+ |apply le_times_to_le_div2
+ [apply lt_O_exp.assumption
+ |simplify.
+
+theorem tech1: \forall a,b,n,m.O < m \to
+n/m \le b \to (a*n)/m \le a*b.
+intros.
+apply le_times_to_le_div2
+ [assumption
+ |
+
+theorem tech2: \forall n,m. O < n \to
+(exp (S n) m) / (exp n m) \le (n + m)/n.
+intros.
+elim m
+ [rewrite < plus_n_O.simplify.
+ rewrite > div_n_n.apply le_n
+ |apply le_times_to_le_div
+ [assumption
+ |apply (trans_le ? (n*(S n)\sup(S n1)/(n)\sup(S n1)))
+ [apply le_times_div_div_times.
+ apply lt_O_exp
+ |simplify in ⊢ (? (? ? %) ?).
+ rewrite > sym_times in ⊢ (? (? ? %) ?).
+ rewrite < eq_div_div_div_times
+ [apply le_times_to_le_div2
+ [assumption
+ |
+
+
+theorem le_log_sigma_p:\forall n,m,p. O < m \to S O < p \to
+log p (exp n m) \le sigma_p n (\lambda i.true) (\lambda i. (m / i)).
+intros.
+elim n
+ [rewrite > exp_n_O
+ [simplify.apply le_n
+ |assumption
+ ]
+ |rewrite > true_to_sigma_p_Sn
+ [apply (trans_le ? (m/n1+(log p (exp n1 m))))
+ [
+*)
\ No newline at end of file