proposition: Lemma CReal_abs_Qabs: forall (x : CReal) (q : Q) (n : Z), CReal_abs x <= inject_Q q -> (Qabs (seq x n) <= q + 2^n)%Q.
proof: Proof. intros x q n Hr. unfold CRealLe in Hr. apply Qnot_lt_le; intros Hq; apply Hr; clear Hr. apply (CRealLt_QR_from_single_dist _ _ n%Z). unfold CReal_abs, CReal_abs_seq; rewrite CReal_red_seq. lra. Qed.
imports: QArith_base Qabs ConstructiveReals ConstructiveCauchyRealsMult Logic.ConstructiveEpsilon ConstructiveCauchyAbs Lia Lqa Qpower QExtra PosExtra ConstructiveExtra Qminmax