proposition: Lemma CReal_abs_right : forall x : CReal, 0 <= x -> CReal_abs x == x.
proof: Proof. intros x Hxnonneg; apply CRealEq_diff; intro n. unfold CReal_abs, CReal_abs_seq, CReal_abs_scale; rewrite CReal_red_seq. pose proof CRealLe_0R_to_single_dist x n Hxnonneg. pose proof Qpower_0_lt 2 n ltac:(lra) as Hpowpos. do 2 apply Qabs_case; intros H1 H2; lra. Qed.
imports: QArith Qabs Qpower ConstructiveCauchyReals ConstructiveCauchyRealsMult Lia Lqa QExtra