From 20389dbd1ad5769688518df414983bb449fd44ef Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 6 Mar 2008 16:21:16 +0000 Subject: [PATCH] fixed --- helm/software/matita/library/nat/neper.ma | 21 ++++++++++++--------- 1 file changed, 12 insertions(+), 9 deletions(-) diff --git a/helm/software/matita/library/nat/neper.ma b/helm/software/matita/library/nat/neper.ma index f200e62d6..4ba2242b4 100644 --- a/helm/software/matita/library/nat/neper.ma +++ b/helm/software/matita/library/nat/neper.ma @@ -17,7 +17,7 @@ include "nat/div_and_mod_diseq.ma". include "nat/binomial.ma". include "nat/log.ma". include "nat/chebyshev.ma". - + theorem sigma_p_div_exp: \forall n,m. sigma_p n (\lambda i.true) (\lambda i.m/(exp (S(S O)) i)) \le ((S(S O))*m*(exp (S(S O)) n) - (S(S O))*m)/(exp (S(S O)) n). @@ -764,7 +764,9 @@ intros;apply eq_sigma_p;intros; rewrite < (eq_plus_minus_minus_minus n x x); [rewrite > exp_plus_times; rewrite > sym_times;rewrite > sym_times in \vdash (? ? (? ? %) ?); - rewrite < eq_div_div_times; + rewrite < sym_times; + rewrite < sym_times in ⊢ (? ? (? ? %) ?); + rewrite < lt_to_lt_to_eq_div_div_times_times; [reflexivity |*:apply lt_O_exp;assumption] |apply le_n @@ -777,8 +779,9 @@ intros;apply eq_sigma_p;intros; elim (bc2 n x) [rewrite > H3;cut (x!*n2 = pi_p x (\lambda i.true) (\lambda i.(n - i))) [rewrite > sym_times in ⊢ (? ? (? (? (? (? % ?) ?) ?) ?) ?); - rewrite > assoc_times;rewrite > sym_times in ⊢ (? ? (? (? (? ? %) ?) ?) ?); - rewrite < eq_div_div_times + rewrite > assoc_times; + rewrite < sym_times in ⊢ (? ? (? (? (? % ?) ?) ?) ?); + rewrite < lt_to_lt_to_eq_div_div_times_times; [rewrite > Hcut;rewrite < assoc_times; cut (pi_p x (λi:nat.true) (λi:nat.n-i)/x!*(a)\sup(x) = pi_p x (λi:nat.true) (λi:nat.(n-i))*pi_p x (\lambda i.true) (\lambda i.a)/x!) @@ -949,7 +952,7 @@ sigma_p (S n) (\lambda x.true) (\lambda k.(exp a (n-k))*(pi_p k (\lambda y.true) (\lambda i.a - (a*i/n)))/k!)/(exp a n). intros;transitivity ((exp a n)*(exp (S n) n)/(exp n n)/(exp a n)) [rewrite > eq_div_div_div_times - [rewrite > sym_times in \vdash (? ? ? (? ? %));rewrite < eq_div_div_times; + [rewrite < sym_times; rewrite < lt_to_lt_to_eq_div_div_times_times; [reflexivity |apply lt_O_exp;assumption |apply lt_O_exp;assumption] @@ -1054,8 +1057,8 @@ intros;rewrite > (neper_sigma_p3 (n*S n) n) [rewrite > H4 [rewrite > sym_times;rewrite < divides_times_to_eq [rewrite < fact_minus - [rewrite > sym_times; - rewrite < eq_div_div_times + [rewrite > sym_times in ⊢ (? ? (? ? %) ?); + rewrite < lt_to_lt_to_eq_div_div_times_times; [reflexivity |apply lt_to_lt_O_minus;apply le_S_S_to_le; assumption @@ -1098,8 +1101,8 @@ intros;rewrite > (neper_sigma_p3 (n*S n) n) [rewrite > H4 [rewrite > sym_times;rewrite < divides_times_to_eq [rewrite < fact_minus - [rewrite > sym_times; - rewrite < eq_div_div_times + [rewrite > sym_times in ⊢ (? ? (? ? %) ?); + rewrite < lt_to_lt_to_eq_div_div_times_times; [reflexivity |apply lt_to_lt_O_minus;apply lt_to_le; assumption -- 2.39.2