From 1f136ddf1cf133efbf10b72b8800e0f8a93b6f68 Mon Sep 17 00:00:00 2001
From: Wilmer Ricciotti <ricciott@cs.unibo.it>
Date: Wed, 12 Dec 2007 18:26:29 +0000
Subject: [PATCH] Progress.

---
 helm/software/matita/library/nat/log.ma   | 30 ++++++++----------
 helm/software/matita/library/nat/neper.ma | 38 ++++++++++++++++++-----
 2 files changed, 43 insertions(+), 25 deletions(-)

diff --git a/helm/software/matita/library/nat/log.ma b/helm/software/matita/library/nat/log.ma
index 3c4f0ad05..53200b161 100644
--- 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
       ]
     ]
diff --git a/helm/software/matita/library/nat/neper.ma b/helm/software/matita/library/nat/neper.ma
index 644db0630..51f65ef4a 100644
--- a/helm/software/matita/library/nat/neper.ma
+++ b/helm/software/matita/library/nat/neper.ma
@@ -294,8 +294,6 @@ intros.
 apply (trans_le ? (log p (((S(S(S O))))\sup(m/n)*((n)\sup(m)))))
   [apply le_log
     [assumption
-    |apply lt_O_exp.
-     apply lt_O_S
     |apply lt_to_le.
      apply lt_exp_Sn_m_SSSO;assumption
     ]
@@ -311,11 +309,11 @@ apply (trans_le ? (log p (((S(S(S O))))\sup(m/n)*((n)\sup(m)))))
   ]
 qed.
 
-theorem le_log_exp_Sn_log_exp_n: \forall a,b,n,p. S O < p \to
-a \le b \to b \le n \to
+theorem le_log_exp_fact_sigma_p: \forall a,b,n,p. S O < p \to
+O < a \to a \le b \to b \le n \to
 log p (exp b n!) - log p (exp a n!) \le
 sigma_p b (\lambda i.leb a i) (\lambda i.S((n!/i)*S(log p (S(S(S O)))))).
-intros 6.
+intros 7.
 elim b
   [simplify.
    apply (lt_O_n_elim ? (lt_O_fact n)).intro.
@@ -331,9 +329,33 @@ elim b
              apply le_log_exp_Sn_log_exp_n
               [apply lt_O_fact
               |assumption
-              |
+              |apply divides_fact;
+                 [apply (trans_le ? ? ? H1);apply leb_true_to_le;assumption
+                 |apply lt_to_le;assumption]]
+            |apply le_log
+              [assumption
+              |cut (O = exp O n!)
+                 [rewrite > Hcut;apply monotonic_exp1;constructor 2;
+                  apply leb_true_to_le;assumption
+                 |elim n
+                    [reflexivity
+                    |simplify;rewrite > exp_plus_times;rewrite < H6;
+                     rewrite > sym_times;rewrite < times_n_O;reflexivity]]]]
+        |apply le_log
+          [assumption
+          |apply monotonic_exp1;apply leb_true_to_le;assumption]]
+      |rewrite > sym_plus;rewrite > sym_plus in \vdash (? ? %);apply le_minus_to_plus;
+       rewrite < minus_plus_m_m;apply H3;apply lt_to_le;assumption]
+    |assumption]
+  |lapply (not_le_to_lt ? ? (leb_false_to_not_le ? ? H5));
+   rewrite > eq_minus_n_m_O
+    [apply le_O_n
+    |apply le_log
+       [assumption
+       |apply monotonic_exp1;assumption]]]]
+qed.
 
-theorem le_log_exp_Sn_log_exp_n: \forall n,m,a,p. O < m \to S O < p \to
+(* theorem le_log_exp_Sn_log_exp_n: \forall n,m,a,p. O < m \to S O < p \to
 divides n m \to
 log p (exp n m) - log p (exp a m) \le
 sigma_p (S n) (\lambda i.leb (S a) i) (\lambda i.S((m/i)*S(log p (S(S(S O)))))).
@@ -354,7 +376,7 @@ elim n
              apply le_log_exp_Sn_log_exp_n.
 
 
-(* a generalization 
+* a generalization 
 theorem le_exp_sigma_p_exp_m: \forall m,n. (exp (S m) n) \le
 sigma_p (S n) (\lambda k.true) (\lambda k.((exp m (n-k))*(exp n k))/(k!)).
 intros.
-- 
2.39.2