proposition: Lemma CRmax_plus : forall {R : ConstructiveReals} (x y z : CRcarrier R), x + CRmax y z == CRmax (x + y) (x + z).
proof: Proof. intros. unfold CRmax. setoid_replace (x + z - (x + y)) with (z-y). - apply (CRmult_eq_reg_r (CR_of_Q _ 2)). + left. apply CR_of_Q_lt; reflexivity. + rewrite CRmult_plus_distr_r. rewrite CRmult_assoc, <- CR_of_Q_mult. setoid_replace ((1 # 2) * 2)%Q with 1%Q. 2: reflexivity. rewrite CRmult_1_r. rewrite CRmult_assoc, <- CR_of_Q_mult. setoid_replace ((1 # 2) * 2)%Q with 1%Q. 2: reflexivity. rewrite (CR_of_Q_plus _ 1 1), CRmult_plus_distr_l, CRmult_1_r. rewrite CRmult_1_r. do 3 rewrite (CRplus_assoc x). apply CRplus_morph. * reflexivity. * do 2 rewrite <- CRplus_assoc. apply CRplus_morph. 2: reflexivity. rewrite (CRplus_comm x). apply CRplus_assoc. - unfold CRminus. rewrite CRopp_plus_distr. rewrite <- CRplus_assoc. apply CRplus_morph. 2: reflexivity. rewrite CRplus_comm, <- CRplus_assoc, CRplus_opp_l. apply CRplus_0_l. Qed.
imports: QArith Qabs ConstructiveReals ConstructiveAbs ConstructiveRealsMorphisms