proposition: Lemma eirr : forall a b, b <> 0%nat -> e = (INR a) / (INR b) -> False.
proof: Proof. intros a b Hb0 Habs. pose (x := INR (fact b) * (e - partial_e b)). assert (0 < x < 1). split. unfold x. apply (minus_exp_sum_pos a) ; intuition. unfold x. apply (minus_exp_sum_one a) ; intuition. destruct (integer_exp_minus_sum a b Hb0 Habs) as (m, Hm). unfold x in *. rewrite Hm in H. apply (integer_0_1 m). assumption. Qed.
imports: PeanoNat Rseries_facts Rsequence_facts Rsequence_subsequence Rpser_usual Reals Rsequence_tactics Rtactic Lra