proposition: Lemma CRmax_contract : forall {R : ConstructiveReals} (x y a : CRcarrier R), CRabs _ (CRmax x a - CRmax y a) <= CRabs _ (x - y).
proof: Proof. intros. unfold CRmax. rewrite (CRabs_morph _ ((x - y + (CRabs _ (a - x) - CRabs _ (a - y))) * CR_of_Q R (1 # 2))). - rewrite CRabs_mult, (CRabs_right (CR_of_Q R (1 # 2))). 2: apply CR_of_Q_le; discriminate. apply (CRle_trans _ ((CRabs _ (x - y) * 1 + CRabs _ (x-y) * 1) * CR_of_Q R (1 # 2))). + apply CRmult_le_compat_r. * apply CR_of_Q_le. discriminate. * apply (CRle_trans _ (CRabs _ (x - y) + CRabs _ (CRabs _ (a - x) - CRabs _ (a - y)))). -- apply CRabs_triang. -- rewrite CRmult_1_r. apply CRplus_le_compat_l. rewrite (CRabs_minus_sym x y). rewrite (CRabs_morph (y-x) ((a-x)-(a-y))). ++ apply CRabs_triang_inv2. ++ unfold CRminus. rewrite (CRplus_comm (a + - x)). rewrite <- CRplus_assoc. apply CRplus_morph. 2: reflexivity. rewrite CRplus_comm, CRopp_plus_distr, <- CRplus_assoc. rewrite CRplus_opp_r, CRopp_involutive, CRplus_0_l. reflexivity. + rewrite <- CRmult_plus_distr_l. rewrite <- (CR_of_Q_plus R 1 1). rewrite CRmult_assoc, <- CR_of_Q_mult. setoid_replace ((1 + 1) * (1 # 2))%Q with 1%Q. 2: reflexivity. rewrite CRmult_1_r. apply CRle_refl. - unfold CRminus. rewrite CRopp_mult_distr_l. rewrite <- CRmult_plus_distr_r. apply CRmult_morph. 2: reflexivity. do 4 rewrite CRplus_assoc. apply CRplus_morph. + reflexivity. + rewrite <- CRplus_assoc. rewrite CRplus_comm, CRopp_plus_distr. rewrite CRplus_assoc. apply CRplus_morph. * reflexivity. * rewrite CRopp_plus_distr. rewrite (CRplus_comm (-a)). rewrite CRplus_assoc, <- (CRplus_assoc (-a)), CRplus_opp_l. rewrite CRplus_0_l. apply CRplus_comm. Qed.
imports: QArith Qabs ConstructiveReals ConstructiveAbs ConstructiveRealsMorphisms