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.