X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fnat%2Fchebyshev_thm.ma;h=dd5f37c3610e742ebc71a7224c23482bb7452d8c;hb=7845d9d0221d94418beecf3d7c3aed3efb2af7fc;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..dd5f37c36 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 
@@ -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