proposition: Lemma CRmin_lt : forall {R : ConstructiveReals} (x y z : CRcarrier R), z < x -> z < y -> z < CRmin x y.
proof: Proof. intros. unfold CRmin. apply (CRmult_lt_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_lt_reg_l _ (CRabs _ (y - x) - (z*CR_of_Q R 2))). unfold CRminus. rewrite CRplus_assoc. rewrite CRplus_opp_l, CRplus_0_r. rewrite (CRplus_comm (CRabs R (y + - x))). rewrite (CRplus_comm (x+y)), CRplus_assoc. rewrite <- (CRplus_assoc (CRabs R (y + - x))), CRplus_opp_r, CRplus_0_l. rewrite <- (CRplus_comm (x+y)). apply CRabs_def1. + unfold CRminus. rewrite <- (CRplus_comm y), CRplus_assoc. apply CRplus_lt_compat_l. apply (CRplus_lt_reg_l R (-x)). rewrite CRopp_mult_distr_l. rewrite <- CRplus_assoc, CRplus_opp_l, CRplus_0_l. rewrite (CR_of_Q_plus R 1 1), CRmult_plus_distr_l. rewrite CRmult_1_r. apply CRplus_le_lt_compat. * apply CRlt_asym. apply CRopp_gt_lt_contravar, H. * apply CRopp_gt_lt_contravar, H. + rewrite CRopp_plus_distr, CRopp_involutive. rewrite CRplus_comm, CRplus_assoc. apply CRplus_lt_compat_l. apply (CRplus_lt_reg_l R (-y)). rewrite CRopp_mult_distr_l. rewrite <- CRplus_assoc, CRplus_opp_l, CRplus_0_l. rewrite (CR_of_Q_plus R 1 1), CRmult_plus_distr_l. rewrite CRmult_1_r. apply CRplus_le_lt_compat. * apply CRlt_asym. apply CRopp_gt_lt_contravar, H0. * apply CRopp_gt_lt_contravar, H0. Qed.
imports: QArith Qabs ConstructiveReals ConstructiveAbs ConstructiveRealsMorphisms