proposition: Lemma integer_exp_minus_sum : forall a b : nat, b <> O -> e = INR a / INR b -> {n | INR (fact b) * (e - partial_e b) = IZR n}.
proof: Proof. intros a b Hb0 Habs. rewrite Habs. rewrite Rmult_minus_distr_l. unfold partial_e. rewrite scal_sum. unfold Rdiv. rewrite Rmult_comm. rewrite Rmult_assoc. rewrite (integer_INR_div b Hb0). destruct (sum_integer_INR_div b) as (m1, Hm1). rewrite Hm1. exists (Z_of_nat a * Z_of_nat (fact (b-1)) - Z_of_nat m1)%Z. unfold Zminus. rewrite plus_IZR. rewrite mult_IZR. rewrite Ropp_Ropp_IZR. repeat rewrite <- INR_IZR_INZ. ring. Qed.
imports: PeanoNat Rseries_facts Rsequence_facts Rsequence_subsequence Rpser_usual Reals Rsequence_tactics Rtactic Lra