X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fnat%2Flog.ma;h=04ab67d5b6b5e2d7281260721459bb754161a360;hb=cb89a1eebdd620d7e1c593fa279e74d4c715b8bf;hp=7f31127b67208a0544b3e4524c07b3bf3a7e25f5;hpb=fb3cf5acfd87741651c5e30ad1911a08e26f6c69;p=helm.git

diff --git a/helm/software/matita/library/nat/log.ma b/helm/software/matita/library/nat/log.ma
index 7f31127b6..04ab67d5b 100644
--- a/helm/software/matita/library/nat/log.ma
+++ b/helm/software/matita/library/nat/log.ma
@@ -214,6 +214,24 @@ split
   ]
 qed.
 
+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.
+    
 theorem le_log: \forall p,n,m. S O < p \to O < n \to n \le m \to 
 log p n \le log p m.
 intros.