proposition: Lemma sum_integer_INR_div : forall n, {m | sum_f_R0 (fun i : nat => / INR (fact i) * INR (fact n)) n = INR m}.
proof: Proof. induction n. exists 1%nat. simpl. field. destruct IHn as (m1, Hm1). rewrite tech5. rewrite fact_simpl. rewrite mult_INR. exists (S n * m1 + 1)%nat. rewrite <- scal_sum. rewrite <- scal_sum in Hm1. rewrite Rmult_assoc. rewrite Hm1. rewrite plus_INR. rewrite mult_INR. do 2 rewrite S_INR. simpl. field. split. apply INR_fact_neq_0. assert (INR n >= 0) by intuition ; intro H1 ; lra. Qed.
imports: PeanoNat Rseries_facts Rsequence_facts Rsequence_subsequence Rpser_usual Reals Rsequence_tactics Rtactic Lra