Some inequalities.

diff --git a/helm/software/matita/library/nat/chebyshev.ma b/helm/software/matita/library/nat/chebyshev.ma
index 567e40ef6bad13927c6098602f9efb7f2bdc7c98..fa935be03784040f76892ff02fb0628b6e2ee687 100644 (file)
--- a/helm/software/matita/library/nat/chebyshev.ma
+++ b/helm/software/matita/library/nat/chebyshev.ma
@@ -676,13 +676,6 @@ apply (trans_eq ? ?
                   [apply prime_to_lt_SO.
                    apply primeb_true_to_prime.
                    assumption
-                  |apply (lt_to_le_to_lt ? x)
-                    [apply prime_to_lt_O.
-                     apply primeb_true_to_prime.
-                     assumption
-                    |apply leb_true_to_le.
-                     assumption
-                    ]
                   |apply le_S_S_to_le.
                    assumption
                   ]
@@ -900,7 +893,6 @@ apply eq_pi_p1;intros
       [apply prime_to_lt_SO.
        apply primeb_true_to_prime.
        assumption
-      |apply lt_to_le.assumption
       |apply le_times_n.
        apply lt_O_S
       ]
@@ -1116,7 +1108,6 @@ cut (
             [apply prime_to_lt_SO.
              apply primeb_true_to_prime.
              assumption
-            |assumption
             |simplify.
              apply le_plus_n_r
             ]
@@ -1274,13 +1265,6 @@ elim H
           [apply prime_to_lt_SO.
            apply primeb_true_to_prime.
            assumption
-          |apply (lt_to_le_to_lt ? i)
-            [apply prime_to_lt_O.
-             apply primeb_true_to_prime.
-             assumption
-            |apply le_S_S_to_le.
-             assumption
-            ]
           |apply le_S.apply le_n
           ]
         ]
@@ -1523,7 +1507,6 @@ rewrite < (eq_log_exp (S(S O))) in ⊢ (? % ?)
   [apply (trans_le ? ((log (S(S O)) (exp ((S(S O))*n) (S(prim ((S(S O))*n)))))))
     [apply le_log
       [apply le_n
-      |apply lt_O_exp.apply lt_O_S
       |apply le_exp_priml.assumption
       ]
     |rewrite > sym_times in ⊢ (? ? %). 
@@ -1555,513 +1538,3 @@ apply (trans_le ? (exp (A n) (S(S O))))
   ]
 qed.
 
-
-(* da spostare *)
-theorem times_exp: \forall n,m,p.exp n p * exp m p = exp (n*m) p.
-intros.elim p
-  [reflexivity
-  |simplify.autobatch
-  ]
-qed.
-
-theorem le_exp_log: \forall p,n. O < n \to
-exp p (
-log n) \le n.
-intros.
-apply leb_true_to_le.
-unfold log.
-apply (f_max_true (\lambda x.leb (exp p x) n)).
-apply (ex_intro ? ? O).
-split
-  [apply le_O_n
-  |apply le_to_leb_true.simplify.assumption
-  ]
-qed.
-
-theorem lt_log_n_n: \forall n. O < n \to log n < n.
-intros.
-cut (log n \le n)
-  [elim (le_to_or_lt_eq ? ? Hcut)
-    [assumption
-    |absurd (exp (S(S O)) n \le n)
-      [rewrite < H1 in ⊢ (? (? ? %) ?).
-       apply le_exp_log.
-       assumption
-      |apply lt_to_not_le.
-       apply lt_m_exp_nm.
-       apply le_n
-      ]
-    ]
-  |unfold log.apply le_max_n
-  ]
-qed.
-
-theorem le_log_n_n: \forall n. log n \le n.
-intro.
-cases n
-  [apply le_n
-  |apply lt_to_le.
-   apply lt_log_n_n.
-   apply lt_O_S
-  ]
-qed.
-
-theorem lt_exp_log: \forall n. n < exp (S(S O)) (S (log n)).
-intro.cases n
-  [simplify.apply le_S.apply le_n
-  |apply not_le_to_lt.
-   apply leb_false_to_not_le.
-   apply (lt_max_to_false ? (S n1) (S (log (S n1))))
-    [apply le_S_S.apply le_n
-    |apply lt_log_n_n.apply lt_O_S
-    ]
-  ]
-qed.
-
-theorem f_false_to_le_max: \forall f,n,p. (∃i:nat.i≤n∧f i=true) \to
-(\forall m. p < m \to f m = false)
-\to max n f \le p.
-intros.
-apply not_lt_to_le.intro.
-apply not_eq_true_false.
-rewrite < (H1 ? H2).
-apply sym_eq.
-apply f_max_true.
-assumption.
-qed.
-
-theorem log_times1: \forall n,m. O < n \to O < m \to
-log (n*m) \le S(log n+log m).
-intros.
-unfold in ⊢ (? (% ?) ?).
-apply f_false_to_le_max
-  [apply (ex_intro ? ? O).
-   split
-    [apply le_O_n
-    |apply le_to_leb_true.
-     simplify.
-     rewrite > times_n_SO.
-     apply le_times;assumption
-    ]
-  |intros.
-   apply lt_to_leb_false.
-   apply (lt_to_le_to_lt ? ((exp (S(S O)) (S(log n)))*(exp (S(S O)) (S(log m)))))
-    [apply lt_times;apply lt_exp_log
-    |rewrite < exp_plus_times.
-     apply le_exp
-      [apply lt_O_S
-      |simplify.
-       rewrite < plus_n_Sm.
-       assumption
-      ]
-    ]
-  ]
-qed.
-  
-theorem log_times: \forall n,m.log (n*m) \le S(log n+log m).
-intros.
-cases n
-  [apply le_O_n
-  |cases m
-    [rewrite < times_n_O.
-     apply le_O_n
-    |apply log_times1;apply lt_O_S
-    ]
-  ]
-qed.
-
-theorem log_exp: \forall n,m.O < m \to
-log ((exp (S(S O)) n)*m)=n+log m.
-intros.
-unfold log in ⊢ (? ? (% ?) ?).
-apply max_spec_to_max.
-unfold max_spec.
-split
-  [split
-    [elim n
-      [simplify.
-       rewrite < plus_n_O.
-       apply le_log_n_n
-      |simplify.
-       rewrite < plus_n_O.
-       rewrite > times_plus_l.
-       apply (trans_le ? (S((S(S O))\sup(n1)*m)))
-        [apply le_S_S.assumption
-        |apply (lt_O_n_elim ((S(S O))\sup(n1)*m))
-          [rewrite > (times_n_O O) in ⊢ (? % ?).
-           apply lt_times
-            [apply lt_O_exp.
-             apply lt_O_S
-            |assumption
-            ]
-          |intro.simplify.apply le_S_S.
-           apply le_plus_n
-          ]
-        ]
-      ]
-    |simplify.
-     apply le_to_leb_true.
-     rewrite > exp_plus_times.
-     apply le_times_r.
-     apply le_exp_log.
-     assumption
-    ]
-  |intros.
-   simplify.
-   apply lt_to_leb_false.
-   apply (lt_to_le_to_lt ? ((exp (S(S O)) n)*(exp (S(S O)) (S(log m)))))
-    [apply lt_times_r1
-      [apply lt_O_exp.apply lt_O_S
-      |apply lt_exp_log.
-      ]
-    |rewrite < exp_plus_times.
-     apply le_exp
-      [apply lt_O_S
-      |rewrite < plus_n_Sm.
-       assumption
-      ]
-    ]
-  ]
-qed.
-
-theorem log_SSO: \forall n. O < n \to 
-log ((S(S O))*n) = S (log n).
-intros.
-change with (log ((exp (S(S O)) (S O))*n)=S (log n)).
-rewrite > log_exp.reflexivity.assumption.
-qed.
-
-theorem or_eq_S: \forall n.\exists m. 
-(n = (S(S O))*m) \lor (n = S((S(S O))*m)).
-intro.
-elim n
-  [apply (ex_intro ? ? O).left.apply times_n_O
-  |elim H.elim H1
-    [apply (ex_intro ? ? a).right.apply eq_f.assumption
-    |apply (ex_intro ? ? (S a)).left.
-     rewrite > H2.simplify.
-     rewrite < plus_n_O.
-     rewrite < plus_n_Sm.
-     reflexivity
-    ]
-  ]
-qed.
-
-theorem lt_O_to_or_eq_S: \forall n.O < n \to \exists m.m < n \land 
-((n = (S(S O))*m) \lor (n = S((S(S O))*m))).
-intros.  
-elim (or_eq_S n).
-elim H1
-  [apply (ex_intro ? ? a).split
-    [rewrite > H2.
-     rewrite > times_n_SO in ⊢ (? % ?).
-     rewrite > sym_times.
-     apply lt_times_l1
-      [apply (divides_to_lt_O a n ? ?)
-        [assumption
-        |apply (witness a n (S (S O))).
-         rewrite > sym_times.
-         assumption
-        ]
-      |apply le_n
-      ]
-    |left.assumption
-    ]
-  |apply (ex_intro ? ? a).split
-    [rewrite > H2.
-     apply (le_to_lt_to_lt ? ((S(S O))*a))
-      [rewrite > times_n_SO in ⊢ (? % ?).
-       rewrite > sym_times. 
-       apply le_times_l.
-       apply le_n_Sn
-      |apply le_n
-      ]
-    |right.assumption
-    ]
-  ]
-qed.
-
-theorem factS: \forall n. fact (S n) = (S n)*(fact n).
-intro.simplify.reflexivity.
-qed.
-
-theorem exp_S: \forall n,m. exp m (S n) = m*exp m n.
-intros.reflexivity.
-qed.
-
-lemma times_SSO: \forall n.(S(S O))*(S n) = S(S((S(S O))*n)).
-intro.simplify.rewrite < plus_n_Sm.reflexivity.
-qed.
-
-theorem fact1: \forall n.
-fact ((S(S O))*n) \le (exp (S(S O)) ((S(S O))*n))*(fact n)*(fact n).
-intro.elim n
-  [rewrite < times_n_O.apply le_n
-  |rewrite > times_SSO.
-   rewrite > factS.
-   rewrite > factS.
-   rewrite < assoc_times.
-   rewrite > factS.
-   apply (trans_le ? (((S(S O))*(S n1))*((S(S O))*(S n1))*(fact (((S(S O))*n1)))))
-    [apply le_times_l.
-     rewrite > times_SSO.
-     apply le_times_r.
-     apply le_n_Sn
-    |rewrite > assoc_times.
-     rewrite > assoc_times.
-     rewrite > assoc_times in ⊢ (? ? %).
-     rewrite > exp_S. 
-     rewrite > assoc_times in ⊢ (? ? %).
-     apply le_times_r.
-     rewrite < assoc_times.
-     rewrite < assoc_times.
-     rewrite < sym_times in ⊢ (? (? (? % ?) ?) ?).
-     rewrite > assoc_times.
-     rewrite > assoc_times.
-     rewrite > exp_S. 
-     rewrite > assoc_times in ⊢ (? ? %).
-     apply le_times_r.
-     rewrite > sym_times in ⊢ (? ? %).
-     rewrite > assoc_times in ⊢ (? ? %).
-     rewrite > assoc_times in ⊢ (? ? %).
-     apply le_times_r.
-     rewrite < assoc_times in ⊢ (? ? %).
-     rewrite < assoc_times in ⊢ (? ? %).
-     rewrite < sym_times in ⊢ (? ? (? (? % ?) ?)).
-     rewrite > assoc_times in ⊢ (? ? %).
-     rewrite > assoc_times in ⊢ (? ? %).
-     apply le_times_r.
-     rewrite > sym_times in ⊢ (? ? (? ? %)).
-     rewrite > sym_times in ⊢ (? ? %).
-     assumption
-    ]
-  ]
-qed.
-
-theorem monotonic_log: monotonic nat le log.
-unfold monotonic.intros.
-elim (le_to_or_lt_eq ? ? H) 0
-  [cases x;intro
-    [apply le_O_n
-    |apply lt_S_to_le.
-     apply (lt_exp_to_lt (S(S O)))
-      [apply le_n
-      |apply (le_to_lt_to_lt ? (S n))
-        [apply le_exp_log.
-         apply lt_O_S
-        |apply (trans_lt ? y)
-          [assumption
-          |apply lt_exp_log
-          ]
-        ]
-      ]
-    ]
-  |intro.rewrite < H1.apply le_n
-  ]
-qed.
-
-theorem lt_O_fact: \forall n. O < fact n.
-intro.elim n
-  [simplify.apply lt_O_S
-  |rewrite > factS.
-   rewrite > (times_n_O O).
-   apply lt_times
-    [apply lt_O_S
-    |assumption
-    ]
-  ]
-qed.
-
-theorem fact2: \forall n.O < n \to
-(exp (S(S O)) ((S(S O))*n))*(fact n)*(fact n) < fact (S((S(S O))*n)).
-intros.elim H
-  [simplify.apply le_S.apply le_n
-  |rewrite > times_SSO.
-   rewrite > factS.
-   rewrite > factS.
-   rewrite < assoc_times.
-   rewrite > factS.
-   rewrite < times_SSO in ⊢ (? ? %).
-   apply (trans_lt ? (((S(S O))*S n1)*((S(S O))*S n1*(S ((S(S O))*n1))!)))
-    [rewrite > assoc_times in ⊢ (? ? %).
-     rewrite > exp_S.
-     rewrite > assoc_times.
-     rewrite > assoc_times.
-     rewrite > assoc_times.
-     apply lt_times_r.
-     rewrite > exp_S.
-     rewrite > assoc_times.
-     rewrite > sym_times in ⊢ (? ? %).
-     rewrite > assoc_times in ⊢ (? ? %).
-     rewrite > assoc_times in ⊢ (? ? %).
-     apply lt_times_r.
-     rewrite > sym_times.
-     rewrite > assoc_times.
-     rewrite > assoc_times.
-     apply lt_times_r.
-     rewrite < assoc_times.
-     rewrite < assoc_times.
-     rewrite > sym_times in ⊢ (? (? (? % ?) ?) ?).
-     rewrite > assoc_times.
-     rewrite > assoc_times.
-     rewrite > sym_times in ⊢ (? ? %).
-     apply lt_times_r.
-     rewrite < assoc_times.
-     rewrite < sym_times.
-     rewrite < assoc_times.
-     assumption
-    |apply lt_times_l1
-      [rewrite > (times_n_O O) in ⊢ (? % ?).
-       apply lt_times
-        [rewrite > (times_n_O O) in ⊢ (? % ?).
-         apply lt_times
-          [apply lt_O_S
-          |apply lt_O_S
-          ]
-        |apply lt_O_fact
-        ]
-      |apply le_n
-      ]
-    ]
-  ]
-qed.
-
-theorem lt_O_log: \forall n. S O < n \to O < log n.
-intros.elim H
-  [simplify.apply lt_O_S
-  |apply (lt_to_le_to_lt ? (log n1))
-    [assumption
-    |apply monotonic_log.
-     apply le_n_Sn
-    ]
-  ]
-qed.
-
-theorem log_fact_SSSO: log (fact (S(S(S O)))) = S (S O).
-reflexivity.
-qed.
-
-lemma exp_SSO_SSO: exp (S(S O)) (S(S O)) = S(S(S(S O))).
-reflexivity.
-qed.
-(*
-theorem log_fact_SSSSO: log (fact (S(S(S(S O))))) = S(S(S(S O))).
-reflexivity.
-qed.
-*)
-theorem log_fact_SSSSSO: log (fact (S(S(S(S(S O)))))) = S(S(S(S O))).
-reflexivity.
-qed.
-
-theorem bof_bof: \forall n.(S(S(S(S O)))) < n \to 
-n \le (S(S(S(S(S(S(S(S O)))))))) \to log (fact n) < n*log n - n.
-intros.
-elim H
-  [rewrite > factS in ⊢ (? (? %) ?). 
-   rewrite > factS in ⊢ (? (? (? ? %)) ?).
-   rewrite < assoc_times in ⊢ (? (? %) ?).
-   rewrite < sym_times in ⊢ (? (? (? % ?)) ?).
-   rewrite > assoc_times in ⊢ (? (? %) ?).
-   change with (exp (S(S O)) (S(S O))) in ⊢ (? (? (? % ?)) ?).
- 
-theorem bof: \forall n.(S(S(S(S O))))) < n \to log (fact n) < n*log n - n.
-intro.apply (nat_elim1 n).
-intros.
-elim (lt_O_to_or_eq_S m)
-  [elim H2.clear H2.
-   elim H4.clear H4.
-   rewrite > H2.
-   apply (le_to_lt_to_lt ? (log ((exp (S(S O)) ((S(S O))*a))*(fact a)*(fact a))))
-    [apply monotonic_log.
-     apply fact1
-    |rewrite > assoc_times in ⊢ (? (? %) ?).
-     rewrite > log_exp.
-     apply (le_to_lt_to_lt ? ((S(S O))*a+S(log a!+log a!)))
-      [apply le_plus_r.
-       apply log_times
-      |rewrite > plus_n_Sm.
-       rewrite > log_SSO.
-       rewrite < times_n_Sm.
-       apply (le_to_lt_to_lt ? ((S(S O))*a+(log a!+(a*log a-a))))
-        [apply le_plus_r.
-         apply le_plus_r.
-         apply H.assumption
-        |apply (lt_to_le_to_lt ? ((S(S O))*a+((a*log a-a)+(a*log a-a))))
-          [apply lt_plus_r.
-           apply lt_plus_l.
-           apply H.
-           assumption.
-          |rewrite > times_SSO_n.
-           rewrite > distr_times_minus.
-           rewrite > sym_plus.
-           rewrite > plus_minus
-            [rewrite > sym_plus.
-             rewrite < assoc_times.
-             apply le_n
-            |rewrite < assoc_times.
-             rewrite > times_n_SO in ⊢ (? % ?).
-             apply le_times
-              [apply le_n
-              |apply lt_O_log.
-               apply (lt_times_n_to_lt_r (S(S O)))
-                [apply lt_O_S
-                |rewrite < times_n_SO.
-                 rewrite < H2.
-                 assumption
-                ]
-              ]
-            ]
-          ]
-          
-             .
-          ]
-        |
-           rewrite < eq_plus_minus_minus_plus.
-           
-       rewrite > assoc_plus.
-       apply lt_plus_r.
-       rewrite > plus_n_O in ⊢ (? (? (? ? (? ? %))) ?).
-       change with
-        (S((S(S O))*a+((S(S O))*log a!)) < (S(S O))*a*log ((S(S O))*a)-(S(S O))*a+k*log ((S(S O))*a)).
-       apply (trans_lt ? (S ((S(S O))*a+(S(S O))*(a*log a-a+k*log a))))
-        [apply le_S_S.
-         apply lt_plus_r.
-         apply lt_times_r.
-         apply H.
-         assumption
-        |
-        
-theorem stirling: \forall n,k.k \le n \to
-log (fact n) < n*log n - n + k*log n.
-intro.
-apply (nat_elim1 n).
-intros.
-elim (lt_O_to_or_eq_S m)
-  [elim H2.clear H2.
-   elim H4.clear H4.
-   rewrite > H2.
-   apply (le_to_lt_to_lt ? (log ((exp (S(S O)) ((S(S O))*a))*(fact a)*(fact a))))
-    [apply monotonic_log.
-     apply fact1
-    |rewrite > assoc_times in ⊢ (? (? %) ?).
-     rewrite > log_exp.
-     apply (le_to_lt_to_lt ? ((S(S O))*a+S(log a!+log a!)))
-      [apply le_plus_r.
-       apply log_times
-      |rewrite < plus_n_Sm.
-       rewrite > plus_n_O in ⊢ (? (? (? ? (? ? %))) ?).
-       change with
-        (S((S(S O))*a+((S(S O))*log a!)) < (S(S O))*a*log ((S(S O))*a)-(S(S O))*a+k*log ((S(S O))*a)).
-       apply (trans_lt ? (S ((S(S O))*a+(S(S O))*(a*log a-a+k*log a))))
-        [apply le_S_S.
-         apply lt_plus_r.
-         apply lt_times_r.
-         apply H.
-         assumption
-        |
-        
-          [
-       
-       a*log a-a+k*log a
-       
-*)
\ No newline at end of file

diff --git a/helm/software/matita/library/nat/log.ma b/helm/software/matita/library/nat/log.ma
index 53200b1613204457774133d2d9fdaad71527918e..39d9b2ecdfae7ecc55209fd8e979581fd28dbbc9 100644 (file)
--- a/helm/software/matita/library/nat/log.ma
+++ b/helm/software/matita/library/nat/log.ma
@@ -159,6 +159,50 @@ cases n
   ]
 qed.
 
+theorem log_times_l: \forall p,n,m.O < n \to O < m \to S O < p \to 
+log p n+log p m \le log p (n*m) .
+intros.
+unfold log in ⊢ (? ? (% ? ?)).
+apply f_m_to_le_max
+  [elim H
+    [rewrite > log_SO
+      [simplify.
+       rewrite < plus_n_O.
+       apply le_log_n_n.
+       assumption
+      |assumption
+      ]
+    |elim H1
+      [rewrite > log_SO
+        [rewrite < plus_n_O.
+         rewrite < times_n_SO.
+         apply le_log_n_n.
+         assumption
+        |assumption
+        ]
+      |apply (trans_le ? (S n1 + S n2))
+        [apply le_plus;apply le_log_n_n;assumption
+        |simplify.
+         apply le_S_S.
+         rewrite < plus_n_Sm.
+         change in ⊢ (? % ?) with ((S n1)+n2).
+         rewrite > sym_plus.
+         apply le_plus_r.
+         change with (n1 < n1*S n2).
+         rewrite > times_n_SO in ⊢ (? % ?).
+         apply lt_times_r1
+          [assumption
+          |apply le_S_S.assumption
+          ]
+        ]
+      ]
+    ]
+  |apply le_to_leb_true.
+   rewrite > exp_plus_times.
+   apply le_times;apply le_exp_log;assumption
+  ]
+qed.
+
 theorem log_exp: \forall p,n,m.S O < p \to O < m \to
 log p ((exp p n)*m)=n+log p m.
 intros.
@@ -286,6 +330,30 @@ intros.elim H1
   [constructor 1
   |apply (trans_le ? ? ? H3);apply le_log_plus;assumption]
 qed.
+         
+theorem log_div: \forall p,n,m. S O < p \to O < m \to m \le n \to
+log p (n/m) \le log p n -log p m.
+intros.
+apply le_plus_to_minus_r.
+apply (trans_le ? (log p ((n/m)*m)))
+  [apply log_times_l
+    [apply le_times_to_le_div
+      [assumption
+      |rewrite < times_n_SO.
+       assumption
+      ]
+    |assumption
+    |assumption
+    ]
+  |apply le_log
+    [assumption
+    |rewrite > (div_mod n m) in ⊢ (? ? %)
+      [apply le_plus_n_r
+      |assumption
+      ]
+    ]
+  ]
+qed.
 
 theorem log_n_n: \forall n. S O < n \to log n n = S O.
 intros.

diff --git a/helm/software/matita/library/nat/neper.ma b/helm/software/matita/library/nat/neper.ma
index 51f65ef4aefeab3967525d226409e3a8b1eb00dc..890d33c66043744e5be6df7db6b5cda72191ad44 100644 (file)
--- a/helm/software/matita/library/nat/neper.ma
+++ b/helm/software/matita/library/nat/neper.ma
@@ -18,6 +18,7 @@ include "nat/iteration2.ma".
 include "nat/div_and_mod_diseq.ma".
 include "nat/binomial.ma".
 include "nat/log.ma".
+include "nat/chebyshev.ma".
 
 theorem sigma_p_div_exp: \forall n,m.
 sigma_p n (\lambda i.true) (\lambda i.m/(exp (S(S O)) i)) \le 
@@ -355,6 +356,123 @@ elim b
        |apply monotonic_exp1;assumption]]]]
 qed.
 
+theorem le_exp_div:\forall n,m,q. O < m \to 
+exp (n/m) q \le (exp n q)/(exp m q).
+intros.
+apply le_times_to_le_div
+  [apply lt_O_exp.
+   assumption
+  |rewrite > times_exp.
+   rewrite < sym_times.
+   apply monotonic_exp1.
+   rewrite > (div_mod n m) in ⊢ (? ? %)
+    [apply le_plus_n_r
+    |assumption
+    ]
+  ]
+qed.
+
+theorem le_log_div_sigma_p: \forall a,b,n,p. S O < p \to
+O < a \to a \le b \to b \le n \to
+log p (b/a) \le
+(sigma_p b (\lambda i.leb a i) (\lambda i.S((n!/i)*S(log p (S(S(S O)))))))/n!.
+intros.
+apply le_times_to_le_div
+  [apply lt_O_fact
+  |apply (trans_le ? (log p (exp (b/a) n!)))
+    [apply log_exp2
+      [assumption
+      |apply le_times_to_le_div
+        [assumption
+        |rewrite < times_n_SO.
+         assumption
+        ]
+      ]
+    |apply (trans_le ? (log p ((exp b n!)/(exp a n!)))) 
+      [apply le_log
+        [assumption
+        |apply le_exp_div.assumption
+        ]
+      |apply (trans_le ? (log p (exp b n!) - log p (exp a n!)))
+        [apply log_div
+          [assumption
+          |apply lt_O_exp.
+           assumption
+          |apply monotonic_exp1.
+           assumption
+          ]
+        |apply le_log_exp_fact_sigma_p;assumption
+        ]
+      ]
+    ]
+  ]
+qed.
+      
+theorem sigma_p_log_div: \forall n,b. S O < b \to
+sigma_p (S n) (\lambda p.(primeb p \land (leb (S n) (p*p)))) (\lambda p.(log b (n/p)))
+\le sigma_p (S n) (\lambda p.primeb p \land (leb (S n) (p*p))) (\lambda p.(sigma_p n (\lambda i.leb p i) (\lambda i.S((n!/i)*S(log b (S(S(S O)))))))/n!
+).
+intros.
+apply le_sigma_p.intros.
+apply le_log_div_sigma_p
+  [assumption
+  |apply prime_to_lt_O.
+   apply primeb_true_to_prime.
+   apply (andb_true_true ? ? H2)
+  |apply le_S_S_to_le.
+   assumption
+  |apply le_n
+  ]
+qed.
+
+theorem sigma_p_log_div1: \forall n,b. S O < b \to
+sigma_p (S n) (\lambda p.(primeb p \land (leb (S n) (p*p)))) (\lambda p.(log b (n/p)))
+\le 
+(sigma_p (S n) (\lambda p.primeb p \land (leb (S n) (p*p))) (\lambda p.(sigma_p n (\lambda i.leb p i) (\lambda i.S((n!/i)))))*S(log b (S(S(S O))))/n!).
+intros.
+apply (trans_le ? (sigma_p (S n) (\lambda p.primeb p \land (leb (S n) (p*p))) (\lambda p.(sigma_p n (\lambda i.leb p i) (\lambda i.S((n!/i)*S(log b (S(S(S O)))))))/n!
+)))
+  [apply sigma_P_log_div.assumption
+  |apply le_times_to_le_div
+    [apply lt_O_fact
+    |rewrite > distributive_times_plus_sigma_p.
+     rewrite < sym_times in ⊢ (? ? %).
+     rewrite > distributive_times_plus_sigma_p.
+     apply le_sigma_p.intros.
+     apply (trans_le ? ((n!*(sigma_p n (λj:nat.leb i j) (λi:nat.S (n!/i*S (log b (S(S(S O)))))))/n!)))
+      [apply le_times_div_div_times.
+       apply lt_O_fact
+      |rewrite > sym_times.
+       rewrite > lt_O_to_div_times
+        [rewrite > distributive_times_plus_sigma_p.
+         apply le_sigma_p.intros.
+         rewrite < times_n_Sm in ⊢ (? ? %).
+         rewrite > plus_n_SO.
+         rewrite > sym_plus.
+         apply le_plus
+          [apply le_S_S.apply le_O_n
+          |rewrite < sym_times.
+           apply le_n
+          ]
+        |apply lt_O_fact
+        ]
+      ]
+    ]
+  ]
+qed.
+     
+(*     
+theorem sigma_p_log_div: \forall n,b. S O < b \to
+sigma_p (S n) (\lambda p.(primeb p \land (leb (S n) (p*p)))) (\lambda p.(log b (n/p)))
+\le (sigma_p (S n) (\lambda i.leb (S n) (i*i)) (\lambda i.(prim i)*n!/i))*S(log b (S(S(S O)))/n!
+).
+intros.
+apply (trans_le ? (sigma_p (S n) (\lambda p.primeb p \land (leb (S n) (p*p))) (\lambda p.(sigma_p n (\lambda i.leb p i) (\lambda i.S((n!/i)))))*S(log b (S(S(S O))))/n!))
+  [apply sigma_p_log_div1
+  |unfold prim.
+*)
+
+
 (* 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