proposition: Lemma CReal_max_sym : forall (x y : CReal), CReal_max x y == CReal_max y x.
proof: Proof. intros. unfold CReal_max. rewrite CReal_abs_minus_sym. ring. Qed.
imports: QArith Qabs Qpower ConstructiveCauchyReals ConstructiveCauchyRealsMult Lia Lqa QExtra