proposition: Lemma AbsIR_minus : forall x y : IR, AbsIR (x[-]y) [=] AbsIR (y[-]x).
proof: Proof. intros. eapply eq_transitive_unfolded. apply AbsIR_inv. apply AbsIR_wd; rational. Qed.
imports: CoRN.reals.Q_in_CReals Coq.QArith.Qabs CoRN.reals.CauchySeq