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