proposition: Lemma AbsIR_eq_inv_x : forall x : IR, x [<=] [0] -> AbsIR x [=] [--]x.
proof: Proof. intros. apply eq_transitive_unfolded with (AbsIR [--]x). apply AbsIR_inv. apply AbsIR_eq_x. astepl ( [--]ZeroR). apply inv_resp_leEq. assumption. Qed.
imports: CoRN.reals.Q_in_CReals Coq.QArith.Qabs CoRN.reals.CauchySeq