proposition: Lemma AbsIR_wdl : forall x y e, x [=] y -> AbsIR x [<] e -> AbsIR y [<] e.
proof: Proof. intros. apply less_wdl with (AbsIR x). assumption. algebra. Qed.
imports: CoRN.reals.Q_in_CReals Coq.QArith.Qabs CoRN.reals.CauchySeq