* please let the library in shape *

diff --git a/helm/software/matita/library/nat/chebyshev_thm.ma b/helm/software/matita/library/nat/chebyshev_thm.ma
index e90b22d9dfaf42d1eec8f2ce2060e3ff3b96a09d..dd5f37c3610e742ebc71a7224c23482bb7452d8c 100644 (file)
--- a/helm/software/matita/library/nat/chebyshev_thm.ma
+++ b/helm/software/matita/library/nat/chebyshev_thm.ma
@@ -205,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)))) + 
@@ -406,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)) 
@@ -961,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