proposition: Lemma CReal_abs_left : forall x : CReal, x <= 0 -> CReal_abs x == -x.
proof: Proof. intros x Hxnonpos. apply CReal_opp_ge_le_contravar in Hxnonpos. rewrite CReal_opp_0 in Hxnonpos. rewrite <- CReal_abs_opp. apply CReal_abs_right, Hxnonpos. Qed.
imports: QArith Qabs Qpower ConstructiveCauchyReals ConstructiveCauchyRealsMult Lia Lqa QExtra