proposition: Lemma CRmorph_min : forall {R1 R2 : ConstructiveReals} (f : @ConstructiveRealsMorphism R1 R2) (a b : CRcarrier R1), CRmorph f (CRmin a b) == CRmin (CRmorph f a) (CRmorph f b).
proof: Proof. intros. unfold CRmin. rewrite CRmorph_mult. apply CRmult_morph. 2: apply CRmorph_rat. unfold CRminus. do 2 rewrite CRmorph_plus. apply CRplus_morph. - apply CRplus_morph. + reflexivity. + reflexivity. - rewrite CRmorph_opp. apply CRopp_morph. rewrite <- CRmorph_abs. apply CRabs_morph. rewrite CRmorph_plus. apply CRplus_morph. + reflexivity. + rewrite CRmorph_opp. apply CRopp_morph, CRmorph_proper. reflexivity. Qed.
imports: QArith Qabs ConstructiveReals ConstructiveAbs ConstructiveRealsMorphisms