Require Export series_correct. Require Export real_value. Open Scope R_scope. Theorem e_correct : infinite_sum (fun i => (1/IZR(fact(i+2))))(real_value number_e_minus2). elim (growing_cv (fun n => sum_f_R0 (fun i => 1/INR(Factorial.fact(i+2))) n)). intros l Hcv. assert (Hsum: infinit_sum (fun i => 1/INR(Factorial.fact(i+2))) l). apply sum_cv_infinit_sum with (1 := Hcv). assert (Hsum2 : infinite_sum (fun i => 1/IZR(fact(i+2))) l). unfold infinite_sum. apply infinit_sum_ext with (2:= Hsum). 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. rewrite (represents_equal number_e_minus2 l). assumption. apply e_correct2. assumption. intros n. simpl. match goal with |- _ <= _ + ?x => assert (Hterm_pos : 0 < x) end. unfold Rdiv; rewrite Rmult_1_l. apply Rinv_0_lt_compat. apply lt_INR_0. pattern 0%nat at 1; replace 0%nat with (0+0)%nat. apply plus_lt_compat. apply lt_O_fact. pattern 0%nat at 1; replace 0%nat with (0*(Factorial.fact(n+2)))%nat. apply mult_lt_compat_r. omega. apply lt_O_fact. ring. ring. fourier. assert (Hbound: forall n, sum_f_R0 (fun i => 1/INR(Factorial.fact(i +2))) n <= 1). intros n. assert (H2l2 : (2<=2)%Z). omega. apply Rle_trans with (1:= partial_sum_bound 2 H2l2 n). replace (INR (Factorial.fact (Zabs_nat 2 - 1)) * (IZR 2 - 1)) with 1. fourier. compute; ring;fail. exists 1; intros v [p Heq]; subst v. apply Hbound. Qed.