proposition: Lemma CRmax_left : forall {R : ConstructiveReals} (x y : CRcarrier R), y <= x -> CRmax x y == x.
proof: Proof. intros. unfold CRmax. apply (CRmult_eq_reg_r (CR_of_Q R 2)). - left. apply CR_of_Q_lt; reflexivity. - rewrite CRmult_assoc, <- CR_of_Q_mult. setoid_replace ((1 # 2) * 2)%Q with 1%Q. 2: reflexivity. rewrite CRmult_1_r. rewrite (CR_of_Q_plus _ 1 1), CRmult_plus_distr_l, CRmult_1_r. rewrite CRplus_assoc. apply CRplus_morph. + reflexivity. + rewrite CRabs_left. * unfold CRminus. rewrite CRopp_plus_distr, CRopp_involutive. rewrite <- CRplus_assoc, CRplus_opp_r, CRplus_0_l. reflexivity. * rewrite <- (CRplus_opp_r x). apply CRplus_le_compat_r. exact H. Qed.
imports: QArith Qabs ConstructiveReals ConstructiveAbs ConstructiveRealsMorphisms