proposition: Lemma CRmin_r : forall {R : ConstructiveReals} (x y : CRcarrier R), CRmin x y <= y.
proof: Proof. intros. unfold CRmin. apply (CRmult_le_reg_r (CR_of_Q R 2)). - 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_comm x). unfold CRminus. rewrite CRplus_assoc. apply CRplus_le_compat_l. apply (CRplus_le_reg_l (-x)). rewrite <- CRplus_assoc, CRplus_opp_l, CRplus_0_l. rewrite <- (CRopp_involutive y), <- CRopp_plus_distr, <- CRopp_plus_distr. apply CRopp_ge_le_contravar. rewrite CRabs_opp, CRplus_comm. apply CRle_abs. Qed.
imports: QArith Qabs ConstructiveReals ConstructiveAbs ConstructiveRealsMorphisms