proposition: Lemma AbsIR_resp_ap_zero : forall x : IR, x [#] [0] -> AbsIR x [#] [0].
proof: Proof. intros. apply ap_symmetric_unfolded; apply less_imp_ap. apply AbsIR_pos; assumption. Qed.
imports: CoRN.reals.Q_in_CReals Coq.QArith.Qabs CoRN.reals.CauchySeq