proposition: Lemma Qabs_Rabs : forall q : Q, inject_Q (Qabs q) == CReal_abs (inject_Q q).
proof: Proof. intro q. apply Qabs_case. - intros. rewrite CReal_abs_right. + reflexivity. + apply inject_Q_le, H. - intros. rewrite CReal_abs_left, opp_inject_Q. + reflexivity. + apply inject_Q_le, H. Qed.
imports: QArith_base Qabs ConstructiveReals ConstructiveCauchyRealsMult Logic.ConstructiveEpsilon ConstructiveCauchyAbs Lia Lqa Qpower QExtra PosExtra ConstructiveExtra