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

diff --git a/helm/software/matita/library/nat/neper.ma b/helm/software/matita/library/nat/neper.ma
index 4ba2242b4..ab14a9ab4 100644
--- a/helm/software/matita/library/nat/neper.ma
+++ b/helm/software/matita/library/nat/neper.ma
@@ -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]]]
@@ -777,7 +777,7 @@ 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 ⊢ (? ? (? (? (? % ?) ?) ?) ?);
@@ -878,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
@@ -944,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) =
@@ -964,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
@@ -1042,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)!))
@@ -1086,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)!))