pretty

[helm.git] / helm / software / matita / library / nat / log.ma

diff --git a/helm/software/matita/library/nat/log.ma b/helm/software/matita/library/nat/log.ma
index 7f31127b67208a0544b3e4524c07b3bf3a7e25f5..04ab67d5b6b5e2d7281260721459bb754161a360 100644 (file)
--- 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.