Progress.

[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 3c4f0ad0552870fe83e6ff2cebd00bb666963c51..53200b1613204457774133d2d9fdaad71527918e 100644 (file)
--- a/helm/software/matita/library/nat/log.ma
+++ b/helm/software/matita/library/nat/log.ma
@@ -271,22 +271,20 @@ apply (lt_exp_to_lt p)
   ]
 qed.
 
-theorem le_log: \forall p,n,m. S O < p \to O < n \to n \le m \to 
+lemma le_log_plus: \forall p,n.S O < p \to log p n \leq log p (S n).
+intros;apply (bool_elim ? (leb (p*(exp p n)) (S n)))
+  [simplify;intro;rewrite > H1;simplify;apply (trans_le ? n)
+    [apply le_log_n_n;assumption
+    |apply le_n_Sn]
+  |intro;unfold log;simplify;rewrite > H1;simplify;apply le_max_f_max_g;
+   intros;apply le_to_leb_true;constructor 2;apply leb_true_to_le;assumption]
+qed.
+
+theorem le_log: \forall p,n,m. S O < p \to n \le m \to 
 log p n \le log p m.
-intros.
-apply le_S_S_to_le.
-apply (lt_exp_to_lt p)
-  [assumption
-  |apply (le_to_lt_to_lt ? n)
-    [apply le_exp_log.
-     assumption
-    |apply (le_to_lt_to_lt ? m)
-      [assumption
-      |apply lt_exp_log.
-       assumption
-      ]
-    ]
-  ]
+intros.elim H1
+  [constructor 1
+  |apply (trans_le ? ? ? H3);apply le_log_plus;assumption]
 qed.
 
 theorem log_n_n: \forall n. S O < n \to log n n = S O.
@@ -331,14 +329,12 @@ apply antisymmetric_le
     [rewrite < (log_n_n i) in ⊢ (? % ?)
       [apply le_log
         [apply (trans_lt ? n);assumption
-        |apply (ltn_to_ltO ? ? H1)
         |apply le_n
         ]
       |apply (trans_lt ? n);assumption
       ]
     |apply le_log
       [apply (trans_lt ? n);assumption
-      |apply (ltn_to_ltO ? ? H1)
       |assumption
       ]
     ]