X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fnat%2Fneper.ma;h=8da13d9ab08e7fdbb4d7f165e75394eb69af15b4;hb=ef3dfcdad5cd42f31ce5575aa1d03247d4547b38;hp=bad55bc49c680d13dc32ed93db1fe515fb505e64;hpb=52cfc3c337a48d52e9d2a8e4e761fa933f161103;p=helm.git

diff --git a/helm/software/matita/library/nat/neper.ma b/helm/software/matita/library/nat/neper.ma
index bad55bc49..8da13d9ab 100644
--- a/helm/software/matita/library/nat/neper.ma
+++ b/helm/software/matita/library/nat/neper.ma
@@ -12,14 +12,12 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/nat/neper".
-
 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 
 ((S(S O))*m*(exp (S(S O)) n) - (S(S O))*m)/(exp (S(S O)) n).
@@ -336,7 +334,7 @@ elim b
             |apply le_log
               [assumption
               |cut (O = exp O n!)
-                 [rewrite > Hcut;apply monotonic_exp1;constructor 2;
+                 [apply monotonic_exp1;constructor 2;
                   apply leb_true_to_le;assumption
                  |elim n
                     [reflexivity
@@ -766,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
@@ -779,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!)
@@ -943,7 +944,7 @@ elim k
               |assumption]
            |assumption]
         |assumption]
-     |do 2 rewrite > false_to_sigma_p_Sn;assumption]]
+     |do 2 try rewrite > false_to_sigma_p_Sn;assumption]]
 qed.
 
 lemma neper_sigma_p3 : \forall a,n.O < a \to O < n \to n \divides a \to (exp (S n) n)/(exp n n) =
@@ -951,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]
@@ -1056,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
@@ -1100,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