From baea5d8f45bafc019ae3a5e39472ed832ba78cb4 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 6 Mar 2008 16:34:15 +0000 Subject: [PATCH] * please let the library in shape * --- helm/software/matita/library/nat/chebyshev_thm.ma | 14 ++------------ 1 file changed, 2 insertions(+), 12 deletions(-) diff --git a/helm/software/matita/library/nat/chebyshev_thm.ma b/helm/software/matita/library/nat/chebyshev_thm.ma index e90b22d9d..dd5f37c36 100644 --- 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 -- 2.39.2