proposition: Lemma AbsIR_inv : forall x : IR, AbsIR x [=] AbsIR [--]x.
proof: Proof. intros. unfold AbsIR in |- *; simpl in |- *; unfold ABSIR in |- *. apply eq_transitive_unfolded with (Max [--][--]x [--]x). apply bin_op_wd_unfolded; algebra. apply Max_comm. Qed.
imports: CoRN.reals.Q_in_CReals Coq.QArith.Qabs CoRN.reals.CauchySeq