proposition: Lemma CReal_abs_opp : forall x : CReal, CReal_abs (-x) == CReal_abs x.
proof: Proof. intros x; apply CRealEq_diff; intro n. unfold CReal_abs, CReal_abs_seq, CReal_abs_scale; unfold CReal_opp, CReal_opp_seq, CReal_opp_scale; do 3 rewrite CReal_red_seq. rewrite Qabs_opp. simplify_Qabs. rewrite Qabs_pos by lra. pose proof Qpower_0_lt 2 n; lra. Qed.
imports: QArith Qabs Qpower ConstructiveCauchyReals ConstructiveCauchyRealsMult Lia Lqa QExtra