proposition: Lemma CRmin_glb : forall {R : ConstructiveReals} (x y z:CRcarrier R), z <= x -> z <= y -> z <= CRmin x 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. apply (CRplus_le_reg_l (CRabs _ (y-x) - (z*CR_of_Q R 2))). unfold CRminus. rewrite CRplus_assoc, CRplus_opp_l, CRplus_0_r. rewrite (CRplus_comm (CRabs R (y + - x) + - (z * CR_of_Q R 2))). rewrite CRplus_assoc, <- (CRplus_assoc (- CRabs R (y + - x))). rewrite CRplus_opp_l, CRplus_0_l. apply CRabs_le. split. + do 2 rewrite CRopp_plus_distr. rewrite CRopp_involutive, (CRplus_comm y), CRplus_assoc. apply CRplus_le_compat_l, (CRplus_le_reg_l y). rewrite <- CRplus_assoc, CRplus_opp_r, CRplus_0_l. rewrite (CR_of_Q_plus R 1 1), CRmult_plus_distr_l. rewrite CRmult_1_r. apply CRplus_le_compat; exact H0. + rewrite (CRplus_comm x), CRplus_assoc. apply CRplus_le_compat_l. apply (CRplus_le_reg_l (-x)). rewrite <- CRplus_assoc, CRplus_opp_l, CRplus_0_l. rewrite CRopp_mult_distr_l. rewrite (CR_of_Q_plus R 1 1), CRmult_plus_distr_l. rewrite CRmult_1_r. apply CRplus_le_compat; apply CRopp_ge_le_contravar; exact H. Qed.
imports: QArith Qabs ConstructiveReals ConstructiveAbs ConstructiveRealsMorphisms