X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fnat%2Fneper.ma;h=ab14a9ab45857b6d65194307ac74e747b7754fd9;hb=647b419e96770d90a82d7a9e5e8843566a9f93ee;hp=f200e62d6d8ff12c137df4f2cde17abdef8dc84c;hpb=c445ba5534cccde19016c92660ab52777af221c0;p=helm.git

diff --git a/helm/software/matita/library/nat/neper.ma b/helm/software/matita/library/nat/neper.ma
index f200e62d6..ab14a9ab4 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).
@@ -280,7 +280,7 @@ rewrite > lt_O_to_div_times
      assumption
     |apply lt_exp_Sn_n_SSSO
     ]
-  |apply (O_lt_times_to_O_lt ? n2).
+  |apply (O_lt_times_to_O_lt ? n1).
    rewrite < H2.
    assumption
   ]
@@ -334,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
@@ -727,10 +727,10 @@ elim k
                     |(*già usata 2 volte: fattorizzare*)
                      elim n
                        [simplify;apply le_n
-                       |apply (bool_elim ? (p n1));intro
+                       |apply (bool_elim ? (p n2));intro
                           [rewrite > true_to_pi_p_Sn
                              [rewrite > (times_n_O O);apply lt_times
-                                [elim (H n1);assumption
+                                [elim (H n2);assumption
                                 |assumption]
                              |assumption]
                           |rewrite > false_to_pi_p_Sn;assumption]]]
@@ -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
@@ -775,10 +777,11 @@ intros;apply eq_sigma_p;intros;
         [rewrite > exp_plus_times;
          unfold bc;
          elim (bc2 n x)
-           [rewrite > H3;cut (x!*n2 = pi_p x (\lambda i.true) (\lambda i.(n - i)))
+           [rewrite > H3;cut (x!*n1 = 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!)
@@ -875,31 +878,31 @@ intros;apply eq_sigma_p;intros;
                              [apply divides_SO_n
                              |elim x
                                 [simplify;apply divides_SO_n
-                                |change in \vdash (? % ?) with (n*(exp n n1));
+                                |change in \vdash (? % ?) with (n*(exp n n2));
                                  rewrite > true_to_pi_p_Sn
                                    [apply divides_times;assumption
                                    |reflexivity]]]
                           |apply lt_O_fact
-                          |apply (witness ? ? n2);symmetry;assumption]]
+                          |apply (witness ? ? n1);symmetry;assumption]]
                     |rewrite > divides_times_to_eq;
                        [apply eq_f2
                           [reflexivity
                           |elim x
                              [simplify;reflexivity
-                             |change in \vdash (? ? % ?) with (a*(exp a n1));
+                             |change in \vdash (? ? % ?) with (a*(exp a n2));
                               rewrite > true_to_pi_p_Sn
                                 [apply eq_f2
                                    [reflexivity
                                    |assumption]
                                 |reflexivity]]]
                        |apply lt_O_fact
-                       |apply (witness ? ? n2);symmetry;assumption]]
+                       |apply (witness ? ? n1);symmetry;assumption]]
                  |apply lt_O_fact
                  |apply lt_O_fact]
               |apply (inj_times_r (pred ((n-x)!)));
                rewrite < (S_pred ((n-x)!))
                  [rewrite < assoc_times;rewrite < sym_times in \vdash (? ? (? % ?) ?);
-                  rewrite < H3;generalize in match H2;elim x
+                  rewrite < H3;generalize in match H2; elim x
                     [rewrite < minus_n_O;simplify;rewrite < times_n_SO;reflexivity
                     |rewrite < fact_minus in H4;
                        [rewrite > true_to_pi_p_Sn
@@ -941,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) =
@@ -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]
@@ -961,15 +964,15 @@ intros;transitivity ((exp a n)*(exp (S n) n)/(exp n n)/(exp a n))
            [elim H2;rewrite > H3;rewrite < times_exp;rewrite > sym_times in ⊢ (? ? (? (? ? ? (λ_:?.? ? %)) ?) ?);
             rewrite > sym_times in ⊢ (? ? ? (? ? ? (λ_:?.? (? (? ? %) ?) ?)));
             transitivity (sigma_p (S n) (λx:nat.true)
-(λk:nat.(exp n n)*(bc n k*(n)\sup(n-k)*(n2)\sup(n)))/exp n n)
+(λk:nat.(exp n n)*(bc n k*(n)\sup(n-k)*(n1)\sup(n)))/exp n n)
               [apply eq_f2
                  [apply eq_sigma_p;intros;
                     [reflexivity
                     |rewrite < assoc_times;rewrite > sym_times;reflexivity]
                  |reflexivity]
-              |rewrite < (distributive_times_plus_sigma_p ? ? ? (\lambda k.bc n k*(exp n (n-k))*(exp n2 n)));
+              |rewrite < (distributive_times_plus_sigma_p ? ? ? (\lambda k.bc n k*(exp n (n-k))*(exp n1 n)));
                transitivity (sigma_p (S n) (λx:nat.true)
-                (λk:nat.bc n k*(n2)\sup(n)*(n)\sup(n-k)))
+                (λk:nat.bc n k*(n1)\sup(n)*(n)\sup(n-k)))
                  [rewrite > (S_pred (exp n n))
                     [rewrite > div_times;apply eq_sigma_p;intros
                        [reflexivity
@@ -1039,7 +1042,7 @@ intros;rewrite > (neper_sigma_p3 (n*S n) n)
                            rewrite > sym_times;apply divides_times
                              [apply divides_SO_n
                              |elim (bc2 n i);
-                                [apply (witness ? ? n2);
+                                [apply (witness ? ? n1);
                                  cut (pi_p i (\lambda y.true) (\lambda i.n-i) = (n!/(n-i)!))
                                    [rewrite > Hcut1;rewrite > H3;rewrite > sym_times in ⊢ (? ? (? (? % ?) ?) ?);
                                     rewrite > (S_pred ((n-i)!))
@@ -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
@@ -1083,7 +1086,7 @@ intros;rewrite > (neper_sigma_p3 (n*S n) n)
                            apply divides_times
                              [apply divides_SO_n
                              |elim (bc2 (S n) i);
-                                [apply (witness ? ? n2);
+                                [apply (witness ? ? n1);
                                  cut (pi_p i (\lambda y.true) (\lambda i.S n-i) = ((S n)!/(S n-i)!))
                                    [rewrite > Hcut1;rewrite > H3;rewrite > sym_times in ⊢ (? ? (? (? % ?) ?) ?);
                                     rewrite > (S_pred ((S n-i)!))
@@ -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