proposition: Lemma CReal_max_contract : forall x y a : CReal, CReal_abs (CReal_max x a - CReal_max y a) <= CReal_abs (x - y).
proof: Proof. intros. unfold CReal_max. rewrite (CReal_abs_morph _ ((x - y + (CReal_abs (a - x) - CReal_abs (a - y))) * inject_Q (1 # 2))). 2: ring. rewrite CReal_abs_mult, (CReal_abs_right (inject_Q (1 # 2))). 2: apply inject_Q_le; discriminate. apply (CReal_le_trans _ ((CReal_abs (x - y) * 1 + CReal_abs (x-y) * 1) * inject_Q (1 # 2))). - apply CReal_mult_le_compat_r. + apply inject_Q_le. discriminate. + apply (CReal_le_trans _ (CReal_abs (x - y) + CReal_abs (CReal_abs (a - x) - CReal_abs (a - y)))). * apply CReal_abs_triang. * rewrite CReal_mult_1_r. apply CReal_plus_le_compat_l. rewrite (CReal_abs_minus_sym x y). rewrite (CReal_abs_morph (y-x) ((a-x)-(a-y))). -- apply CReal_abs_triang_inv2. -- unfold CReal_minus. rewrite (CReal_plus_comm (a + - x)). rewrite <- CReal_plus_assoc. apply CReal_plus_morph. 2: reflexivity. rewrite CReal_plus_comm, CReal_opp_plus_distr, <- CReal_plus_assoc. rewrite CReal_plus_opp_r, CReal_opp_involutive, CReal_plus_0_l. reflexivity. - rewrite <- CReal_mult_plus_distr_l, <- inject_Q_plus. rewrite CReal_mult_assoc, <- inject_Q_mult. setoid_replace ((1 + 1) * (1 # 2))%Q with 1%Q. 2: reflexivity. rewrite CReal_mult_1_r. apply CRealLe_refl. Qed.
imports: QArith Qabs Qpower ConstructiveCauchyReals ConstructiveCauchyRealsMult Lia Lqa QExtra