proposition: Lemma CRmax_lub_lt : forall {R : ConstructiveReals} (x y z : CRcarrier R), x < z -> y < z -> CRmax x y < z.
proof: Proof. intros. unfold CRmax. 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 _ (-y -x)). unfold CRminus. rewrite CRplus_assoc, <- (CRplus_assoc (-x)), <- (CRplus_assoc (-x)). rewrite CRplus_opp_l, CRplus_0_l, <- CRplus_assoc, CRplus_opp_l, CRplus_0_l. apply CRabs_def1. + rewrite (CRplus_comm y), (CRplus_comm (-y)), CRplus_assoc. apply CRplus_lt_compat_l. apply (CRplus_lt_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_lt_compat. * apply CRlt_asym, H0. * exact H0. + rewrite CRopp_plus_distr, CRopp_involutive. rewrite CRplus_assoc. apply CRplus_lt_compat_l. apply (CRplus_lt_reg_l _ x). 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_lt_compat. * apply CRlt_asym, H. * exact H. Qed.
imports: QArith Qabs ConstructiveReals ConstructiveAbs ConstructiveRealsMorphisms