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