proposition: Lemma CRmin_right : forall {R : ConstructiveReals} (x y : CRcarrier R), y <= x -> CRmin x y == y.
proof: Proof. intros. unfold CRmin. 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 CRabs_left. + unfold CRminus. do 2 rewrite CRopp_plus_distr. rewrite (CRplus_comm x y). rewrite CRplus_assoc. apply CRplus_morph. * reflexivity. * do 2 rewrite CRopp_involutive. rewrite CRplus_comm, CRplus_assoc, CRplus_opp_l, CRplus_0_r. reflexivity. + rewrite <- (CRplus_opp_r x). apply CRplus_le_compat. * exact H. * apply CRle_refl. Qed.
imports: QArith Qabs ConstructiveReals ConstructiveAbs ConstructiveRealsMorphisms