proposition: Lemma CRmax_lub : forall {R : ConstructiveReals} (x y z:CRcarrier R), x <= z -> y <= z -> CRmax x y <= z.
proof: Proof. intros. unfold CRmax. apply (CRmult_le_reg_r (CR_of_Q _ 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 (-x-y)). rewrite <- CRplus_assoc. unfold CRminus. rewrite <- CRopp_plus_distr, CRplus_opp_l, CRplus_0_l. apply CRabs_le. split. + repeat rewrite CRopp_plus_distr. do 2 rewrite CRopp_involutive. 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 (CR_of_Q_plus _ 1 1), CRmult_plus_distr_l, CRmult_1_r. rewrite CRopp_plus_distr. apply CRplus_le_compat; apply CRopp_ge_le_contravar; assumption. + rewrite (CRplus_comm y), CRopp_plus_distr, CRplus_assoc. apply CRplus_le_compat_l. apply (CRplus_le_reg_l y). rewrite <- CRplus_assoc, CRplus_opp_r, CRplus_0_l. rewrite (CR_of_Q_plus _ 1 1), CRmult_plus_distr_l, CRmult_1_r. apply CRplus_le_compat; assumption. Qed.
imports: QArith Qabs ConstructiveReals ConstructiveAbs ConstructiveRealsMorphisms