proposition: Lemma AbsIR_Qabs : forall (a:Q), AbsIR (inj_Q IR a)[=]inj_Q IR (Qabs a).
proof: Proof. intros a. apply Qabs_case; intros H. apply AbsIR_eq_x. stepl (inj_Q IR [0]). apply inj_Q_leEq. assumption. now apply (inj_Q_nring IR 0). stepr ([--](inj_Q IR a)). apply AbsIR_eq_inv_x. stepr (inj_Q IR [0]). apply inj_Q_leEq. assumption. now apply (inj_Q_nring IR 0). apply eq_symmetric. apply inj_Q_inv. Qed.
imports: CoRN.reals.Q_in_CReals Coq.QArith.Qabs CoRN.reals.CauchySeq