proposition: Lemma exp_remain_sum : forall n, n <> O -> INR (fact n) * (e - partial_e n) < 1 / INR n.
proof: Proof. intros b Hb0. unfold partial_e, e, exp. destruct (exist_exp 1) as (x, Hexp). simpl. unfold exp_in in *. assert (Hgeom : (infinite_sum (fun i => (/INR (S b)) ^ i) (1 / (1 - /INR (S b))))). apply (geometric_sum (/INR (S b))). unfold Rabs. destruct (Rcase_abs (/INR (S b))) as [H1|[H1|H1]]. assert (H : (- /INR (S b) < 0 )) by intuition. eapply (Rlt_trans) ; [apply H|intuition]. replace 1 with (/1) by intuition. apply Rinv_lt_contravar. rewrite Rmult_1_l. intuition. destruct b. destruct Hb0. reflexivity. rewrite S_INR. assert (INR (S b) > 0) by intuition. lra. rewrite H1. lra. assert (He : (infinite_sum (fun i : nat => / INR (fact i)) x)). intros eps Heps. destruct (Hexp eps Heps) as (N, Hexp1). exists N. intros n Hn. generalize (Hexp1 n Hn). intros H1. assert (Hrew : (sum_f_R0 (fun i : nat => / INR (fact i) * 1 ^ i) n = sum_f_R0 (fun i : nat => / INR (fact i)) n)). apply sum_eq. intros. rewrite pow1. intuition. rewrite <- Hrew. apply H1. clear Hexp. pose (Un := fun n : nat => / INR (fact (n))). pose (UUn := fun n : nat => Un (S b + n)%nat). assert (Hluu : Rser_cv UUn (x - sum_f_R0 Un b)). apply (Rser_cv_shifts b Un). assumption. assert (Hlu : Rser_cv Un x). apply He. assert (HRser : Rser_cv (fun k => Un (S b+ k)%nat) (Rser_rem Un x Hlu b)). apply (Rser_rem_cv Un). assert (Rser_cv Un (Rser_rem Un x Hlu b + sum_f_R0 Un b)). apply Rser_cv_shifts_rev. assumption. assert (H1 : (x = Rser_rem Un x Hlu b + sum_f_R0 Un b)). apply Rser_cv_unique with Un ; assumption. rewrite H1. unfold Un. ring_simplify. assert (Hlmachin : Rser_cv Un x). intuition. apply Rser_cv_scal_compat_l with Un x (INR (fact b)) in Hlmachin. fold Un. apply Rle_lt_trans with ((INR (fact b) * Rser_rem Un x Hlu)%Rseq b). reflexivity. rewrite <- (Rser_rem_scal_compat_l Un x (INR (fact b)) Hlmachin). pose (Vn := (fun n0 : nat => INR (fact b) * / INR (fact n0) )). assert (Hlv : (Rser_cv Vn (INR (fact b) * x))). unfold Vn. apply Rser_cv_scal_compat_l. assumption. unfold Un. fold Vn. pose (Wn := (fun i : nat => /(INR (S b)) * (/ INR (S b)) ^ i)). assert (Hlw : Rser_cv Wn (( /INR (S b) *(1/ (1 - / INR (S b)))))). unfold Wn. apply Rser_cv_scal_compat_l. apply Rser_cv_ext with (fun i : nat => (/ INR (S b)) ^ i). intro ; reflexivity. apply Hgeom. eapply Rlt_le_trans with (/ INR (S b) * (1 / (1 - / INR (S b)))). apply (Rser_Rser_rem_lt_le Wn Vn _ _ _ _). intros k Hkn. unfold Vn, Wn. apply identite. assumption. exists (S (S b)). intuition. unfold Vn, Wn. apply identite1. apply Hlw. field_simplify. replace (INR (S b) - 1) with (INR b). right. reflexivity. rewrite S_INR. ring. INR_solve. split. apply not_0_INR. intuition. rewrite S_INR. unfold Rminus. rewrite Rplus_assoc. intro H2. ring_simplify in H2. revert H2. change (INR b <> 0). INR_solve. Qed.
imports: PeanoNat Rseries_facts Rsequence_facts Rsequence_subsequence Rpser_usual Reals Rsequence_tactics Rtactic Lra