Require Export realbasis. Require Export proof_utils. Require Export real_facts. Require Export add_correct. Require Export fact. Open Scope Z_scope. Theorem fact_pos : forall p n, p = Z_of_nat (fact n) -> 0 < p. intros; subst; apply (inj_lt 0); apply lt_O_fact. Qed. Theorem fact_step : forall n, (fact n * (n + 1) = fact (n+1))%nat. intros; rewrite plus_comm; simpl; rewrite mult_comm; simpl; auto. Qed. Theorem fact_gt_1 : forall p, 2 <= p -> 1 < (Z_of_nat (fact (Zabs_nat p))). intros p; elim p using (well_founded_ind (Zwf_well_founded 2)). clear p. intros p Hrec Hle; elim (Z_le_gt_dec p 2); intros Hcase. replace p with 2; compute; auto. omega. assert (Zabs_nat p - 1 = Zabs_nat (p - 1))%nat. rewrite Zabs_nat_minus. auto. omega. replace (Zabs_nat p) with (S (Zabs_nat (p - 1))). rewrite fact_simpl. replace (S (Zabs_nat (p - 1))) with (1+Zabs_nat (p - 1))%nat. rewrite inj_mult. assert (1 < Z_of_nat (fact (Zabs_nat (p - 1)))). apply Hrec; unfold Zwf; omega. apply Zlt_le_trans with (Z_of_nat (1 + (Zabs_nat (p - 1)))*1). rewrite Zmult_1_r. rewrite inj_plus. rewrite Zabs_nat_minus. rewrite inj_minus1. repeat rewrite Z_of_nat_Zabs_nat; simpl Z_of_nat; omega. rewrite Zabs_nat_1. assert (0 < Zabs_nat p)%nat. apply (Zabs_nat_lt 0);omega. omega. omega. apply Zmult_le_compat_l. omega. rewrite inj_plus. apply Zplus_le_0_compat. omega. omega. ring_nat. rewrite <- H. match goal with |- S ?x = _ => change (S x) with (1 + x)%nat end. rewrite le_plus_minus_r. auto. assert (0 < Zabs_nat p)%nat. apply (Zabs_nat_lt 0);omega. omega. Qed. Theorem fact_step_minus : forall n, (1 <= n -> fact (n - 1) * n = fact n)%nat. intros n H; induction H; simpl; auto. rewrite <- minus_n_O; ring_nat. Qed. Theorem lt_0_inv_fact : forall k, (0 < 1 /INR(fact k))%R. intros k; unfold Rdiv. apply Rlt_mult_inv_pos. fourier. rewrite INR_IZR_INZ. apply (IZR_lt 0). apply (inj_lt 0). apply lt_O_fact. Qed. Theorem fact_under_estimate : forall k i, 0<= k -> Z_of_nat (fact(Zabs_nat k)) * k^Z_of_nat i <= Z_of_nat (fact(i+(Zabs_nat k))). intros k i Hkpos; induction i. simpl. rewrite Zmult_1_r; auto with zarith. pattern (S i) at 1;replace (S i) with (i + 1)%nat. rewrite inj_plus. rewrite Zpower_exp. rewrite Zmult_assoc. replace (k^Z_of_nat 1) with k. simpl (S i + Zabs_nat k)%nat. rewrite fact_simpl. rewrite inj_mult. rewrite Zmult_comm. apply Zmult_le_compat. replace (S (i + Zabs_nat k)) with (1 + (i + Zabs_nat k))%nat. repeat rewrite inj_plus. simpl Z_of_nat. rewrite Z_of_nat_Zabs_nat. omega. assumption. ring_nat. exact IHi. assumption. apply Zmult_le_0_compat. apply Zle_0_nat. apply Zpower_le_0_compat; assumption. simpl; unfold Zpower_pos; simpl; ring. omega. omega. ring_nat. Qed. Theorem fact_pm1_fact_p : forall p fact_pm1, 2 <= p -> fact_pm1 = Z_of_nat (fact (Zabs_nat (p - 1))) -> fact_pm1 * p = Z_of_nat (fact (Zabs_nat p)). intros p fact_pm1 Hpge2 Hfact. rewrite Hfact. pattern p at 2; rewrite <- Z_of_nat_Zabs_nat. rewrite <- inj_mult. rewrite Zabs_nat_minus. rewrite Zabs_nat_1. rewrite fact_step_minus. auto. apply (Zabs_nat_le 1). omega. omega. omega. Qed. Theorem partial_sum_bound : forall p, 2 <= p -> forall n, (sum_f_R0 (fun i => (1/INR(fact (i+Zabs_nat p)))%R) n <= 1/(INR (fact(Zabs_nat p - 1))*(IZR p -1)))%R. intros p Hpeg2. assert (Hpos : (forall i, 0 <= 1/(INR(fact(i + Zabs_nat p))))%R). intros n; apply Rlt_le; apply lt_0_inv_fact. intros n. replace (1/(INR(fact (Zabs_nat p - 1))*(IZR p - 1)))%R with (1/(INR(fact (Zabs_nat p))) *(IZR p/(IZR p - 1)))%R. assert (H1ltp : 1 < p). omega. assert (Hfactpos : (0 < INR(fact(Zabs_nat p)))%R). apply lt_INR_0. apply lt_O_fact. apply Rle_trans with (2:= tech_exp (INR (fact (Zabs_nat p))) p n H1ltp Hfactpos). apply sum_Rle. intros n' _; unfold Rdiv; repeat rewrite Rmult_1_l. apply Rle_Rinv. apply Rmult_lt_0_compat. apply (lt_INR 0); apply lt_O_fact. rewrite power_IZR; apply pow_lt; apply (IZR_lt 0); omega. apply (lt_INR 0); apply lt_O_fact. repeat rewrite INR_IZR_INZ. rewrite <- mult_IZR. apply IZR_le. apply fact_under_estimate. omega. replace (INR(fact (Zabs_nat p))) with (INR(fact (Zabs_nat p - 1)*(Zabs_nat p))). repeat rewrite INR_IZR_INZ. rewrite inj_mult. rewrite Z_of_nat_Zabs_nat. rewrite mult_IZR. field. assert ((IZR p <> 0)%R). apply not_O_IZR; omega. assert ((IZR p + -1 <> 0)%R). replace (-1)%R with (IZR (-1)). rewrite <- plus_IZR. apply not_O_IZR; omega. apply (Ropp_Ropp_IZR 1). assert ((IZR (Z_of_nat (fact (Zabs_nat p - 1))) <> 0)%R). rewrite <- INR_IZR_INZ. apply not_O_INR. apply fact_neq_0. repeat apply prod_neq_R0;auto. omega. rewrite fact_step_minus. auto. apply (Zabs_nat_le 1). omega. Qed. Theorem infinit_sum_inv_fact_bound : forall p r, 2 <= p -> infinit_sum (fun i => 1/INR(fact (i+Zabs_nat p)))%R r -> (0 < r <= 1/(INR (fact(Zabs_nat p-1))*(IZR p - 1)))%R. intros p r Hpeg2 Hinf. generalize (infinit_sum_cv _ _ Hinf). intros Hcv. split. apply Rlt_le_trans with (1/(INR(fact(Zabs_nat p))))%R. apply lt_0_inv_fact. assert (Hpos : (forall i, 0 <= 1/(INR(fact(i + Zabs_nat p))))%R). intros n. apply Rlt_le. apply lt_0_inv_fact. exact (sum_incr _ 0 r Hcv Hpos). simpl sum_f_R0. assert ((forall n, sum_f_R0 (fun i => (1/INR(fact (i+Zabs_nat p)))%R) n <= 1/(INR (fact(Zabs_nat p - 1))*(IZR p -1)))%R). apply partial_sum_bound; auto; fail. apply Rle_cv_lim with (Vn:= (fun i:nat => 1/(INR(fact (Zabs_nat p - 1))*(IZR p -1)))%R) (1:= H) (2:=Hcv). intros eps; exists 0%nat; intros n _; rewrite R_dist_eq. auto with real. Qed. Theorem tech_bound : forall n r u, (0 < IZR u)%R -> (0 < r <= 1/IZR u)%R -> 8*n <= u -> (2 * (IZR n * r) <= 1/4)%R. intros; dec_tac. apply Rmult_le_reg_l with 4%R. fourier. replace (4*(1/4))%R with 1%R;[idtac | field; auto with real1]. replace (4 * (2 * (IZR n * r)))%R with (IZR (8 *n) *r)%R. apply Rle_trans with (IZR u * r)%R. apply Rmult_le_compat_r. fourier. apply IZR_le; assumption. replace 1%R with (IZR u * (1/IZR u))%R. apply Rmult_le_compat_l. fourier. assumption. auto with real. field. apply Rlt_neq_0; assumption. rewrite mult_IZR;simpl IZR;ring. Qed. Ltac apply_e_correct1' e_series' := match goal with e_correct1 : _, id : represents ?v ?vr, id1 : infinit_sum _ ?r |- represents (e_series' ?v (?n, ?p, ?f)) ?w => replace w with (vr + IZR n * r)%R; [ apply e_correct1;clear e_correct1;auto with real1 | idtac] end. Theorem e_series_body_correct : forall (e_series : stream idigit -> Z*Z*Z -> stream idigit), (forall v vr r n p fact_pm1, fact_pm1 = (Z_of_nat (fact (Zabs_nat (p-1)))) -> 4 * n <= fact_pm1 * (p - 1) -> 2 <= p -> 1 <= n -> represents v vr -> infinit_sum (fun i => (1/INR(fact (i+Zabs_nat p)))%R) r -> (vr + (IZR n) *r <= 1)%R -> represents (e_series v (n,p,fact_pm1))(vr+(IZR n)*r)%R) -> forall v vr r n p fact_pm1, fact_pm1 = (Z_of_nat (fact (Zabs_nat (p-1)))) -> 8 * n <= fact_pm1 * (p - 1) -> 2 <= p -> 1 <= n -> represents v vr -> infinit_sum (fun i => (1/INR(fact (i+Zabs_nat p)))%R) r -> (vr + (IZR n) *r <= 1)%R -> represents (series_body (Z*Z*Z) e_series v (2*n, p, fact_pm1)) (vr+(IZR n)*r)%R. intros e_series' e_correct1. intros v vr r n p fact_pm1 Hfact Hle Hpge2 Hnge1 Hv Hsum Hin_res. unfold series_body. assert (Hfactpos : 0 < fact_pm1). clear e_correct1. rewrite Hfact. apply (inj_lt 0). apply lt_O_fact. assert (Hprodpos : (0 < IZR(fact_pm1 *(p-1)))%R). clear e_correct1. apply (IZR_lt 0); apply Zmult_lt_O_compat. assumption. omega. assert (Hboundr : (2*(IZR n* r) <= 1/4)%R). clear e_correct1. apply tech_bound with (fact_pm1 * (p - 1)). assumption. generalize (infinit_sum_inv_fact_bound _ _ Hpge2 Hsum). rewrite INR_IZR_INZ; rewrite mult_IZR; rewrite Hfact. rewrite <- Z_R_minus; simpl IZR. rewrite Zabs_nat_minus. intros; assumption. omega. assumption. assert (Hnrpos : (0 < IZR n * r)%R). apply Rmult_lt_0_compat. apply (IZR_lt 0); omega. generalize (infinit_sum_inv_fact_bound _ _ Hpge2 Hsum). intros; dec_tac; assumption. destruct v as [ [ | | ] v'']; inversion Hv. destruct v'' as [ [ | | ] v3]; inversion_to_variable v3. (* case : L::L *) add_fact v3. constructor';[idtac | clear e_correct1]. apply_e_correct1' e_series'. omega. omega. rewrite mult_IZR; simpl IZR; rewrite Rmult_assoc. dec_tac; fourier. unfold lift, alpha; autorewrite with real1; rewrite mult_IZR; simpl IZR; field; auto with real1;fail. unfold lift, alpha; autorewrite with real1. rewrite double_plus_distr. dec_tac; split; autorewrite with real1; fourier. (* case : L::R *) add_fact v3. constructor';[idtac | clear e_correct1]. apply_e_correct1' e_series'. omega. omega. rewrite mult_IZR; simpl IZR; rewrite Rmult_assoc. dec_tac; unfold lift, alpha; autorewrite with real1; fourier. unfold lift, alpha; rewrite mult_IZR; simpl IZR; field; auto with real1;fail. unfold lift, alpha; autorewrite with real1. dec_tac; split; fourier. (* case : L::C *) add_fact v3. constructor';[idtac | clear e_correct1]. apply_e_correct1' e_series'. omega. omega. rewrite mult_IZR; simpl IZR; rewrite Rmult_assoc. dec_tac; fourier. unfold lift, alpha; autorewrite with real1; rewrite mult_IZR; simpl IZR; field; auto with real1;fail. rewrite double_plus_distr. unfold lift, alpha; autorewrite with real1; dec_tac; split;fourier. (* case : R *) constructor';[idtac | clear e_correct1]. apply_e_correct1' e_series'. omega. omega. rewrite mult_IZR; replace r0 with (2*vr -1)%R; [simpl IZR; rewrite Rmult_assoc| subst vr;ring]. fourier. unfold lift, alpha; autorewrite with real1; field; auto with real1; fail. unfold lift, alpha; autorewrite with real1; rewrite mult_IZR; simpl IZR; field; auto with real1; fail. split. match goal with |- (0 <= ?v)%R => replace v with (r0+ 2*(IZR n *r))%R end. dec_tac; auto with real1; fail. unfold lift, alpha; autorewrite with real1 real2;ring;fail. replace r0 with (2*vr -1)%R;[idtac|subst vr ; unfold lift, alpha; autorewrite with real1; field;auto with real1;fail]. unfold lift, alpha; autorewrite with real1 real2;fourier. destruct v'' as [ [ | | ] v3]; inversion_to_variable v3. (* case : C::L *) add_fact v3. constructor';[idtac | clear e_correct1]. apply_e_correct1' e_series'. replace 4%R with (IZR 4);[idtac | simpl IZR; ring]. omega. omega. rewrite mult_IZR; simpl IZR; rewrite Rmult_assoc. dec_tac; fourier. unfold lift, alpha; rewrite mult_IZR; simpl IZR; field; auto with real1. unfold lift, alpha; rewrite double_plus_distr. autorewrite with real1. rewrite double_plus_distr. autorewrite with real1. dec_tac; split;fourier. (* case : C::R *) add_fact v3. constructor';[idtac | clear e_correct1]. apply_e_correct1' e_series'. replace 4%R with (IZR 4);[idtac | simpl IZR; ring]. omega. omega. rewrite mult_IZR; replace r1 with (2*r0 -1)%R; [simpl IZR; rewrite Rmult_assoc| subst r0;unfold lift, alpha; field;auto with real1;fail]. unfold lift, alpha; autorewrite with real1 real2. dec_tac; fourier. unfold lift, alpha; rewrite mult_IZR; simpl IZR; field; auto with real1. autorewrite with real1. rewrite double_plus_distr with (y:= (IZR n * r)%R). repeat rewrite double_plus_distr with (y:= (1/4*1)%R). unfold lift, alpha; autorewrite with real1. dec_tac; split; fourier. (* case C::C *) add_fact v3. constructor';[idtac | clear e_correct1]. apply_e_correct1' e_series'. replace 4%R with (IZR 4);[idtac | simpl IZR; ring]. omega. omega. rewrite mult_IZR; simpl IZR; rewrite Rmult_assoc. dec_tac; fourier. unfold lift, alpha; rewrite mult_IZR; simpl IZR; field; auto with real1;fail. unfold lift, alpha. rewrite double_plus_distr. autorewrite with real1. rewrite double_plus_distr with (y:= (1/4*1)%R). autorewrite with real1. dec_tac; split;fourier. Defined. Theorem e_correct1_aux : forall v vr r n p fact_pm1, fact_pm1 = (Z_of_nat (fact (Zabs_nat (p-1)))) -> 4 * n <= fact_pm1 * (p-1) -> 2 <= p -> 1 <= n -> represents v vr -> infinit_sum (fun i => (1/INR(fact (i+Zabs_nat p)))%R) r -> (vr + (IZR n)*r <= 1)%R -> represents (e_series v (n, p, fact_pm1)) (vr+(IZR n)*r)%R. cofix. intros v vr r n p fact_pm1 Hfact Hinv Hpge2 Hnge1 Hrepr Hinf Hin. rewrite (str_dec_thm (e_series v (n, p, fact_pm1))); unfold str_decompose. lazy zeta beta iota delta [e_series]; fold e_series. elim (Z_le_gt_dec (8*n) (fact_pm1 *(p - 1))). intros Hle. change (represents (str_decompose (series_body (Z*Z*Z) e_series v (2*n,p,fact_pm1))) (vr + IZR n * r)). rewrite <- str_dec_thm. exact (e_series_body_correct e_series e_correct1_aux v vr r n p fact_pm1 Hfact Hle Hpge2 Hnge1 Hrepr Hinf Hin). intros Hgt. replace (vr + IZR n * r)%R with ((vr + (IZR n)/(IZR (fact_pm1 * p))) + (IZR n) * (r - 1/(IZR (fact_pm1 * p))))%R; [idtac | clear e_correct1_aux]. change (represents (str_decompose (series_body (Z*Z*Z) e_series (v+rat_to_stream n (fact_pm1*(p-1)+fact_pm1)) (2*n,p+1, fact_pm1*(p-1)+fact_pm1))) (vr + IZR n/IZR(fact_pm1*p) +IZR n *(r-1/IZR (fact_pm1 *p))) ); rewrite <- str_dec_thm. apply (e_series_body_correct e_series e_correct1_aux (v + rat_to_stream n (fact_pm1 * (p-1) + fact_pm1))%S (vr + (IZR n)/(IZR (fact_pm1 * p)))%R (r - 1/(IZR (fact_pm1 * p)))%R n (p + 1) (fact_pm1 * (p-1) + fact_pm1)); clear e_correct1_aux. ring (p + 1 - 1). pattern p at 1; rewrite <- (Z_of_nat_Zabs_nat p). rewrite Hfact. assert (Habs_p_pos : (Zabs_nat 1 < Zabs_nat p)%nat). apply Zabs_nat_lt; omega. assert (Hfactpm1: Z_of_nat (Zabs_nat p) - 1 = Z_of_nat (Zabs_nat (p - 1))). rewrite Zabs_nat_minus; auto with zarith. rewrite inj_minus1; auto with zarith arith. rewrite Hfactpm1. rewrite <- inj_mult. rewrite <- inj_plus. rewrite Zabs_nat_minus. rewrite Zabs_nat_1. assert (Haux1 : (fact(Zabs_nat p - 1) = fact(Zabs_nat p - 1) * 1)%nat). ring_nat. pattern (fact(Zabs_nat p -1)) at 2; rewrite Haux1; clear Haux1. rewrite <- mult_plus_distr_l. rewrite <- (plus_comm 1). rewrite le_plus_minus_r; auto. rewrite (fact_step_minus (Zabs_nat p)). auto;fail. rewrite <- Zabs_nat_1. apply lt_le_weak. apply Zabs_nat_lt. omega. omega. omega. omega. apply Zle_trans with (2* (fact_pm1 * (p - 1))). omega. replace (fact_pm1*(p-1)+fact_pm1) with (fact_pm1*p);[idtac|ring]. rewrite Zmult_permute. rewrite <- Zmult_assoc. apply Zmult_le_compat_l. apply Zmult_le_compat; omega. rewrite Hfact. apply Zle_0_nat. omega. omega. apply add_correct. assumption. replace (fact_pm1*(p-1)+fact_pm1) with (fact_pm1*p);[idtac|ring]. apply rat_to_stream_correct. split. omega. apply Zle_trans with (4*n). omega. apply Zle_trans with (1:= Hinv). apply Zmult_le_compat_l. omega. rewrite Hfact. apply Zle_0_nat. apply Zmult_lt_O_compat. rewrite Hfact. apply (inj_lt 0). apply lt_O_fact. omega. apply Rle_trans with (2:= Hin). apply Rplus_le_compat_l. replace (IZR n/IZR(fact_pm1 * p))%R with (IZR n * (1/IZR(fact_pm1 * p)))%R. apply Rmult_le_compat_l. apply (IZR_le 0). omega. 2: field;auto with real1. 5: field;auto with real1. generalize (infinit_sum_step _ _ Hinf); intros Hinf_step. simpl (0 + Zabs_nat p)%nat in Hinf_step. assert (Hext:forall n, ((fun i => 1/INR(fact (i+1+Zabs_nat p))) n= (fun i => 1/INR(fact (i+(Zabs_nat (p + 1))))) n)%R). intros i; simpl; replace (i+1+Zabs_nat p)%nat with (i + (Zabs_nat (p + 1)))%nat. auto. rewrite Zabs_nat_plus. rewrite Zabs_nat_1. ring. omega. omega. generalize (infinit_sum_ext (fun i => 1/INR(fact(i + 1 + Zabs_nat p)))%R (fun i => 1/INR(fact(i + (Zabs_nat (p + 1)))))%R _ Hext Hinf_step). intros Hinf_step'. assert (Hpp1ge2 : 2 <= p + 1). omega. generalize (infinit_sum_inv_fact_bound (p+1) _ Hpp1ge2 Hinf_step'). intros Hint'. rewrite INR_IZR_INZ in Hint'. dec_tac. rewrite <- fact_step_minus in H. rewrite <- Zabs_nat_1 in H. rewrite <- Zabs_nat_minus in H. rewrite inj_mult in H. rewrite <- Hfact in H. rewrite Z_of_nat_Zabs_nat in H. fourier. omega. omega. rewrite <- Zabs_nat_1. apply Zabs_nat_le. omega. rewrite mult_IZR. apply prod_neq_R0. apply not_O_IZR. assert (0 < fact_pm1). rewrite Hfact. apply (inj_lt 0). apply lt_O_fact. omega. apply not_O_IZR. omega. apply infinit_sum_ext with (fun i => 1/INR(fact ((i+1)+Zabs_nat p)))%R. replace (IZR (fact_pm1 * p)) with (INR (fact (0 + (Zabs_nat p)))). intros i; rewrite Zabs_nat_plus. rewrite Zabs_nat_1. rewrite (plus_comm (Zabs_nat p)). rewrite plus_assoc. auto. omega. omega. simpl. rewrite INR_IZR_INZ. rewrite Hfact. pattern p at 3; rewrite <- Z_of_nat_Zabs_nat. rewrite <- inj_mult. rewrite Zabs_nat_minus. rewrite Zabs_nat_1. rewrite fact_step_minus. auto. rewrite <- Zabs_nat_1; apply Zabs_nat_le. omega. omega. omega. rewrite fact_pm1_fact_p. rewrite <- INR_IZR_INZ. apply infinit_sum_step with (An := (fun i => 1/INR (fact (i + Zabs_nat p)))%R). assumption. assumption. assumption. match goal with |- (?x <= 1)%R => replace x with (vr + IZR n * r)%R end. assumption. unfold Rdiv; ring. rewrite mult_IZR. apply prod_neq_R0. apply not_O_IZR. assert (0 < fact_pm1). rewrite Hfact. apply (inj_lt 0). apply lt_O_fact. omega. apply not_O_IZR. omega. Qed. Definition infinite_sum (f:Z->Rdefinitions.R)(v:Rdefinitions.R) : Prop := infinit_sum (fun n => f (Z_of_nat n)) v. Definition fact := Zfact. Theorem e_correct1 : forall v vr r y n, 4 * y <= fact(n-1) * (n-1) -> 2 <= n -> 1 <= y -> represents v vr -> infinite_sum (fun i => 1/IZR(fact (i+n)))%R r -> (vr + (IZR y)*r <= 1)%R -> represents (e_series v (y, n, fact(n-1))) (vr+(IZR y)*r). unfold fact, infinite_sum. intros v vr r y n Hmodulus Hn Hy Hrep Hsum Hbounds. apply e_correct1_aux; auto. rewrite Zfact_fact_nat; auto with zarith. apply infinit_sum_ext with (2:= Hsum). intros n'; rewrite Zfact_fact_nat. rewrite <- INR_IZR_INZ. rewrite Zabs_nat_plus. replace (Zabs_nat (Z_of_nat n')) with n'; auto. unfold Zabs_nat, Z_of_nat; destruct n'; auto. rewrite nat_of_P_o_P_of_succ_nat_eq_succ; auto. auto with zarith. omega. omega. Qed. Theorem Zabs_nat_Z_of_nat : forall n, Zabs_nat (Z_of_nat n) = n. intros n; destruct n; unfold Zabs_nat, Z_of_nat; auto. rewrite nat_of_P_o_P_of_succ_nat_eq_succ; auto. Qed. Theorem e_correct2 : forall r, infinite_sum (fun i => (1/IZR(fact(i+2)))%R) r -> represents number_e_minus2 r. intros r H. unfold number_e_minus2. replace r with ((1/2+1/6)+(IZR 1)*((r-(1/2))-1/6))%R;[idtac | ring]. pattern 6 at 2; replace 6 with (fact (4-1)). apply (e_correct1 ((rat_to_stream 1 2)+(rat_to_stream 1 6))(1/2+1/6) (r-1/2-1/6) 1 4). unfold fact; rewrite Zfact_fact_nat. compute; intros; discriminate. omega. omega. omega. apply add_correct. replace 2%R with (IZR 2);[idtac | simpl IZR; ring]. replace 1%R with (IZR 1);[idtac | simpl IZR; ring]. apply rat_to_stream_correct. omega. omega. replace 6%R with (IZR 6);[idtac | simpl IZR; ring]. replace 1%R with (IZR 1);[idtac | simpl IZR; ring]. apply rat_to_stream_correct. omega. omega. fourier. unfold infinite_sum. apply infinit_sum_ext with (fun i => (fun j =>(1/INR(Factorial.fact(j + Zabs_nat 3)))%R) (i+1)%nat). intros n; unfold Zabs_nat, nat_of_P; simpl. replace (n +1 + 3)%nat with (n+4)%nat;[idtac|ring;fail]. unfold fact; rewrite Zfact_fact_nat. rewrite <- INR_IZR_INZ. rewrite Zabs_nat_plus; auto with zarith. rewrite Zabs_nat_Z_of_nat. trivial. omega. replace (1/6)%R with ((fun j =>(1/INR(Factorial.fact(j + Zabs_nat 3)))) 0%nat)%R. apply infinit_sum_step with (An := (fun j => (1/INR(Factorial.fact(j + Zabs_nat 3)))%R)). replace (1/2)%R with ((fun j =>(1/INR(Factorial.fact(j + Zabs_nat 2)))) 0%nat)%R. apply infinit_sum_ext with (fun i => (fun j =>(1/INR(Factorial.fact(j + Zabs_nat 2)))%R) (i+1)%nat). intros n; unfold Zabs_nat, nat_of_P; simpl. replace (n+1+2)%nat with (n+3)%nat;[auto|ring]. apply infinit_sum_step with (An := (fun j => (1/INR(Factorial.fact(j + Zabs_nat 2)))%R)). apply infinit_sum_ext with (2:= H). intros n; unfold fact; rewrite Zfact_fact_nat. rewrite <- INR_IZR_INZ. rewrite Zabs_nat_plus. rewrite Zabs_nat_Z_of_nat; trivial;fail. omega. omega. omega. auto;fail. compute; field. replace ((2+1+1+1+1)*6)%R with (IZR 36). apply not_O_IZR. omega. simpl IZR; ring. simpl IZR; match goal with |- (?x <=1)%R => replace x with r end. assert (Hint: (0 < r <= 1/(INR(Factorial.fact(Zabs_nat 2 -1)) *(IZR 2 - 1)))%R). apply infinit_sum_inv_fact_bound. auto with zarith. apply infinit_sum_ext with (2:= H). intros n; unfold fact; rewrite Zfact_fact_nat. rewrite <- INR_IZR_INZ; rewrite Zabs_nat_plus. rewrite Zabs_nat_Z_of_nat; trivial;fail. omega. omega. omega. destruct Hint as [H1 H2]. match goal with id : (r <= 1/?x)%R |- _ => replace x with 1%R in id end. fourier. compute; ring. ring. compute; trivial. Qed.