From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Thu, 6 Mar 2008 16:21:16 +0000 (+0000)
Subject: fixed
X-Git-Tag: make_still_working~5556
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=20389dbd1ad5769688518df414983bb449fd44ef;p=helm.git

fixed
---

diff --git a/helm/software/matita/library/nat/neper.ma b/helm/software/matita/library/nat/neper.ma
index f200e62d6..4ba2242b4 100644
--- a/helm/software/matita/library/nat/neper.ma
+++ b/helm/software/matita/library/nat/neper.ma
@@ -17,7 +17,7 @@ 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 
 ((S(S O))*m*(exp (S(S O)) n) - (S(S O))*m)/(exp (S(S O)) n).
@@ -764,7 +764,9 @@ intros;apply eq_sigma_p;intros;
       rewrite < (eq_plus_minus_minus_minus n x x);
         [rewrite > exp_plus_times;
          rewrite > sym_times;rewrite > sym_times in \vdash (? ? (? ? %) ?);
-         rewrite < eq_div_div_times;
+         rewrite < sym_times;
+         rewrite < sym_times in ⊢ (? ? (? ? %) ?);
+         rewrite < lt_to_lt_to_eq_div_div_times_times;
            [reflexivity
            |*:apply lt_O_exp;assumption]
         |apply le_n
@@ -777,8 +779,9 @@ intros;apply eq_sigma_p;intros;
          elim (bc2 n x)
            [rewrite > H3;cut (x!*n2 = pi_p x (\lambda i.true) (\lambda i.(n - i)))
               [rewrite > sym_times in ⊢ (? ? (? (? (? (? % ?) ?) ?) ?) ?);
-               rewrite > assoc_times;rewrite > sym_times in ⊢ (? ? (? (? (? ? %) ?) ?) ?);
-               rewrite < eq_div_div_times
+               rewrite > assoc_times;
+               rewrite < sym_times in ⊢ (? ? (? (? (? % ?) ?) ?) ?);
+               rewrite < lt_to_lt_to_eq_div_div_times_times;
                  [rewrite > Hcut;rewrite < assoc_times;
                   cut (pi_p x (λi:nat.true) (λi:nat.n-i)/x!*(a)\sup(x)
                     = pi_p x (λi:nat.true) (λi:nat.(n-i))*pi_p x (\lambda i.true) (\lambda i.a)/x!)
@@ -949,7 +952,7 @@ sigma_p (S n) (\lambda x.true)
 (\lambda k.(exp a (n-k))*(pi_p k (\lambda y.true) (\lambda i.a - (a*i/n)))/k!)/(exp a n).
 intros;transitivity ((exp a n)*(exp (S n) n)/(exp n n)/(exp a n))
   [rewrite > eq_div_div_div_times
-     [rewrite > sym_times in \vdash (? ? ? (? ? %));rewrite < eq_div_div_times;
+     [rewrite < sym_times; rewrite < lt_to_lt_to_eq_div_div_times_times;
         [reflexivity
         |apply lt_O_exp;assumption
         |apply lt_O_exp;assumption]
@@ -1054,8 +1057,8 @@ intros;rewrite > (neper_sigma_p3 (n*S n) n)
                                          [rewrite > H4
                                             [rewrite > sym_times;rewrite < divides_times_to_eq
                                                [rewrite < fact_minus
-                                                  [rewrite > sym_times;
-                                                   rewrite < eq_div_div_times
+                                                  [rewrite > sym_times in ⊢ (? ? (? ? %) ?);
+                                                   rewrite < lt_to_lt_to_eq_div_div_times_times;
                                                      [reflexivity
                                                      |apply lt_to_lt_O_minus;apply le_S_S_to_le;
                                                       assumption
@@ -1098,8 +1101,8 @@ intros;rewrite > (neper_sigma_p3 (n*S n) n)
                                          [rewrite > H4
                                             [rewrite > sym_times;rewrite < divides_times_to_eq
                                                [rewrite < fact_minus
-                                                  [rewrite > sym_times;
-                                                   rewrite < eq_div_div_times
+                                                  [rewrite > sym_times in ⊢ (? ? (? ? %) ?);
+                                                   rewrite < lt_to_lt_to_eq_div_div_times_times;
                                                      [reflexivity
                                                      |apply lt_to_lt_O_minus;apply lt_to_le;
                                                       assumption