proposition: Lemma AbsIR_cancel_ap_zero : forall x : IR, AbsIR x [#] [0] -> x [#] [0].
proof: Proof. intros. apply un_op_strext_unfolded with AbsIR. apply ap_wdr_unfolded with ZeroR. assumption. apply eq_symmetric_unfolded; apply AbsIRz_isz. Qed.
imports: CoRN.reals.Q_in_CReals Coq.QArith.Qabs CoRN.reals.CauchySeq