proposition: Lemma CReal_abs_bound : forall (x : CReal), QBound (CReal_abs_seq x) (CReal_abs_scale x).
proof: Proof. intros x n. unfold CReal_abs_seq, CReal_abs_scale. rewrite Qabs_involutive. apply (bound x). Qed.
imports: QArith Qabs Qpower ConstructiveCauchyReals ConstructiveCauchyRealsMult Lia Lqa QExtra