proposition: Lemma minus_exp_sum_pos : forall a b : nat, b <> O -> INR (fact b) * (e - partial_e b) > 0.
proof: Proof. intros a b Hb0. unfold e, partial_e, exp. destruct (exist_exp 1) as (y, Hexp). unfold exp_in in *. simpl. apply Rmult_gt_0_compat ; [apply INR_fact_lt_0|]. unfold infinite_sum in Hexp. assert (H : y <= sum_f_R0 (fun n : nat => / INR (fact n)) b -> False). intro Habs. assert (H1 : /INR (fact (S b)) > 0) by (apply inv_INR_fact_pos). generalize (Hexp (/INR (fact (S b))) H1) ; clear Hexp ; intro Hexp. destruct Hexp as (N, Hexp). assert (Hmax : ((max N (S b)) >= N)%nat). intuition. generalize (Hexp (max N (S b)) Hmax). clear Hexp. intros Hexp. unfold R_dist in *. unfold Rabs in *. replace (sum_f_R0 (fun i : nat => / INR (fact i) * 1 ^ i) (max N (S b))) with (sum_f_R0 (fun n : nat => / INR (fact n)) (max N (S b))) in * by (apply Rseq_sum_ext ; intros n; rewrite pow1; ring). destruct (Rcase_abs (sum_f_R0 (fun i : nat => / INR (fact i)) (max N (S b)) - y)) as [H|H]. apply Rle_minus in Habs. assert (sum_f_R0 (fun n : nat => / INR (fact n)) b - y < sum_f_R0 (fun i : nat => / INR (fact i)) (max N (S b)) - y). unfold Rminus. apply Rplus_lt_compat_r. apply sum_max. intuition. apply inv_INR_fact_pos. lra. apply Rminus_lt_plus in Hexp. apply (Rplus_le_compat_r (/ INR (fact (S b)))) in Habs. assert (sum_f_R0 (fun i : nat => / INR (fact i)) (max N (S b)) >= sum_f_R0 (fun n : nat => / INR (fact n)) b + / INR (fact (S b))). rewrite <- tech5. apply sum_max1. intros. left. apply inv_INR_fact_pos. assert (H2 : (sum_f_R0 (fun i : nat => / INR (fact i)) (max N (S b)) < sum_f_R0 (fun n : nat => / INR (fact n)) b + / INR (fact (S b)))). eapply Rlt_le_trans. apply Hexp. apply Habs. apply Rlt_not_ge in H2. apply H2. assumption. apply Rgt_minus. apply Rlt_gt. apply Rnot_le_gt. assumption. Qed.
imports: PeanoNat Rseries_facts Rsequence_facts Rsequence_subsequence Rpser_usual Reals Rsequence_tactics Rtactic Lra