proposition: Lemma CReal_opp_bound : forall (x : CReal), QBound (CReal_opp_seq x) (CReal_opp_scale x).
proof: Proof. intros x k. unfold CReal_opp_seq, CReal_opp_scale. pose proof (bound x k) as Hxbnd. rewrite Qabs_Qlt_condition in Hxbnd |- *. lra. Qed.
imports: QArith Qpower Qabs Qround Logic.ConstructiveEpsilon Lia Lqa QExtra ConstructiveExtra