proposition: Lemma CRmin_sym : forall {R : ConstructiveReals} (x y : CRcarrier R), CRmin x y == CRmin y x.
proof: Proof. intros. unfold CRmin. apply CRmult_morph. 2: reflexivity. rewrite CRabs_minus_sym. unfold CRminus. rewrite (CRplus_comm x y). reflexivity. Qed.
imports: QArith Qabs ConstructiveReals ConstructiveAbs ConstructiveRealsMorphisms