proposition: Lemma AbsIR_eq_zero : forall x : IR, AbsIR x [=] [0] -> x [=] [0].
proof: Proof. intros. apply AbsIR_approach_zero; intros. astepl ZeroR; apply less_leEq; auto. Qed.
imports: CoRN.reals.Q_in_CReals Coq.QArith.Qabs CoRN.reals.CauchySeq