proposition: Lemma CReal_abs_Qabs_diff: forall (x y : CReal) (q : Q) (n : Z), CReal_abs (x - y) <= inject_Q q -> (Qabs (seq x n - seq y n) <= q + 2*2^n)%Q.
proof: Proof. intros x y q n Hr. unfold CRealLe in Hr. apply Qnot_lt_le; intros Hq; apply Hr; clear Hr. apply (CRealLt_QR_from_single_dist _ _ (n+1)%Z). unfold CReal_abs, CReal_abs_seq; rewrite CReal_red_seq. unfold CReal_minus, CReal_plus, CReal_plus_seq; rewrite CReal_red_seq, Qred_correct. unfold CReal_opp, CReal_opp_seq; rewrite CReal_red_seq. ring_simplify (n + 1 - 1)%Z. rewrite Qpower_plus by lra. ring_simplify; change (seq x n + - seq y n)%Q with (seq x n - seq y n)%Q. lra. Qed.
imports: QArith_base Qabs ConstructiveReals ConstructiveCauchyRealsMult Logic.ConstructiveEpsilon ConstructiveCauchyAbs Lia Lqa Qpower QExtra PosExtra ConstructiveExtra Qminmax