Even if the error is not localized, it was not a good idea to make the unification...

[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..d96fb28c233c93dee7137da008533a0c4799b4ad 100644 (file)
--- a/helm/software/matita/library/nat/log.ma
+++ b/helm/software/matita/library/nat/log.ma
@@ -214,6 +214,38 @@ split
   ]
 qed.
 
+theorem eq_log_exp: \forall p,n.S O < p \to
+log p (exp p n)=n.
+intros.
+rewrite > times_n_SO in ⊢ (? ? (? ? %) ?).
+rewrite > log_exp
+  [rewrite > log_SO
+    [rewrite < plus_n_O.reflexivity
+    |assumption
+    ]
+  |assumption
+  |apply le_n
+  ]
+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.