proposition: Lemma minus_exp_sum_one : forall a b : nat, b <> 0%nat -> e = INR a / INR b -> INR (fact b) * (e - partial_e b) < 1.
proof: Proof. intros a b Hb0 Habs. eapply Rlt_le_trans. apply exp_remain_sum. assumption. unfold Rdiv. rewrite Rmult_1_l. apply inv_inf_1. assumption. Qed.
imports: PeanoNat Rseries_facts Rsequence_facts Rsequence_subsequence Rpser_usual Reals Rsequence_tactics Rtactic Lra