+theorem log_exp1: \forall p,n,m.S O < p \to
+log p (exp n m) \le m*S(log p n).
+intros.elim m
+ [simplify in ⊢ (? (? ? %) ?).
+ rewrite > log_SO
+ [apply le_O_n
+ |assumption
+ ]
+ |simplify.
+ apply (trans_le ? (S (log p n+log p (n\sup n1))))
+ [apply log_times.assumption
+ |apply le_S_S.
+ apply le_plus_r.
+ assumption
+ ]
+ ]
+qed.
+