proposition: Lemma AbsIR_approach_zero : forall x, (forall e, [0] [<] e -> AbsIR x [<=] e) -> x [=] [0].
proof: Proof. intros. apply leEq_imp_eq. apply approach_zero_weak. intros e H0. eapply leEq_transitive; [ apply leEq_AbsIR | exact (H e H0) ]. astepl ( [--]ZeroR); astepr ( [--][--]x); apply inv_resp_leEq. apply approach_zero_weak. intros e H0. eapply leEq_transitive; [ apply inv_leEq_AbsIR | exact (H e H0) ]. Qed.
imports: CoRN.reals.Q_in_CReals Coq.QArith.Qabs CoRN.reals.CauchySeq