proposition: Lemma CRmin_lt_r : forall {R : ConstructiveReals} (x y : CRcarrier R), CRmin x y < y -> CRmin x y == x.
proof: Proof. intros. unfold CRmin. unfold CRmin in H. apply (CRmult_eq_reg_r (CR_of_Q R 2)). - left; apply CR_of_Q_pos; 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 R 1 1), CRmult_plus_distr_l, CRmult_1_r. rewrite CRabs_right. + unfold CRminus. rewrite CRopp_plus_distr, CRplus_assoc, <- (CRplus_assoc y). rewrite CRplus_opp_r, CRplus_0_l, CRopp_involutive. reflexivity. + apply (CRmult_lt_compat_r (CR_of_Q R 2)) in H. 2: apply CR_of_Q_pos; reflexivity. intro abs. contradict H. apply (CRle_trans _ (x + y - CRabs R (y - x))). * rewrite CRabs_left. 2: apply CRlt_asym, abs. unfold CRminus. rewrite CRopp_involutive, CRplus_comm. rewrite CRplus_assoc, <- (CRplus_assoc (-x)), CRplus_opp_l. rewrite CRplus_0_l, (CR_of_Q_plus R 1 1), CRmult_plus_distr_l. rewrite CRmult_1_r. apply CRle_refl. * rewrite CRmult_assoc, <- CR_of_Q_mult. setoid_replace ((1 # 2) * 2)%Q with 1%Q. 2: reflexivity. rewrite CRmult_1_r. apply CRle_refl. Qed.
imports: QArith Qabs ConstructiveReals ConstructiveAbs ConstructiveRealsMorphisms