proposition: Lemma CReal_abs_minus_sym : forall x y : CReal, CReal_abs (x - y) == CReal_abs (y - x).
proof: Proof. intros x y. setoid_replace (x - y) with (-(y-x)). - rewrite CReal_abs_opp. reflexivity. - ring. Qed.
imports: QArith Qabs Qpower ConstructiveCauchyReals ConstructiveCauchyRealsMult Lia Lqa QExtra