X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fnat%2Fchebyshev_thm.ma;h=129336d8e70fc15ac9d61f24d27cd5da6ccba153;hb=7288b45eacf9f7dcd118b3b89b81ff19ae9d6ce5;hp=248c9e3c67e041649752ac3f7262a7a789546c49;hpb=10f29fdd78ee089a9a94446207b543d33d6c851c;p=helm.git

diff --git a/helm/software/matita/library/nat/chebyshev_thm.ma b/helm/software/matita/library/nat/chebyshev_thm.ma
index 248c9e3c6..129336d8e 100644
--- a/helm/software/matita/library/nat/chebyshev_thm.ma
+++ b/helm/software/matita/library/nat/chebyshev_thm.ma
@@ -12,8 +12,6 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/nat/chebyshev_thm/".
-
 include "nat/neper.ma".
 
 definition C \def \lambda n.pi_p (S n) primeb 
@@ -79,7 +77,7 @@ cut (\forall m.pi_p (S n) primeb
            [apply (bool_elim ? (leb ((S n1)*(S n1)) m))
               [intro;rewrite > true_to_pi_p_Sn in \vdash (? ? ? (? % ?))
                  [rewrite > false_to_pi_p_Sn in \vdash (? ? ? (? ? %))
-                    [rewrite > H1;rewrite > H2;rewrite < assoc_times;reflexivity
+                    [rewrite > H1;rewrite < assoc_times;reflexivity
                     |rewrite > H;lapply (leb_true_to_le ? ? H2);
                      lapply (le_to_not_lt ? ? Hletin);
                      apply (bool_elim ? (leb (S m) (S n1 * S n1)))
@@ -207,6 +205,7 @@ apply (trans_le ? (sigma_p (S n) (λx:nat.primeb x∧leb (S n) (x*x)) (λx:nat.1
               |rewrite > andb_sym;apply le_O_n]
            |apply sigma_p_log_div;assumption]]]]
 qed.
+(* 
  
 lemma le_prim_n_stima : \forall n,b. S O < b \to b \leq n \to
 prim n \leq (S (((S (S (S (S O))))*(S (log b (pred n)))) + 
@@ -408,18 +407,6 @@ cut (\forall b,i,k.S O < b \to S O < i \to
      |assumption]]
 qed.
                   
-lemma eq_div_div_times : \forall x,y,z.O < z \to O < y \to x/y = (z*x)/(z*y).
-intros.rewrite > (div_mod x y) in \vdash (? ? ? %);
-  [rewrite > distr_times_plus;rewrite > sym_times;rewrite > assoc_times;
-   rewrite > sym_times in ⊢ (? ? ? (? (? (? ? %) ?) ?));
-   rewrite > div_plus_times
-     [reflexivity
-     |generalize in match H;cases z;intros
-        [elim (not_le_Sn_O ? H2)
-        |apply lt_times_r;apply lt_mod_m_m;assumption]]
-  |assumption]
-qed.
-                  
 alias num (instance 0) = "natural number".
 lemma le_sigma_p_lemma1 : \forall n,b. S O < b \to b*b < n \to
             (sigma_p n (\lambda x.leb (S n) (x*x)) 
@@ -963,3 +950,4 @@ apply (trans_le ? ? ? (le_S_S ? ? (le_prim_stima ? 2 ? ?)))
                 |apply (trans_le ? ? ? ? H);apply lt_O_S]]]]]
   apply (trans_le ? ? ? ? Hcut);
 *)
+*)
\ No newline at end of file