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