proposition: Lemma Qmax_contract : forall (a b c : Q), Qabs (Qmax a b - Qmax a c) <= Qabs (b - c).
proof: Proof. intros. apply Qabs_Qle_condition. split. - apply Qmax_case. + intros. apply Qmax_case. intros. unfold Qminus. rewrite Qplus_opp_r. apply (Qopp_le_compat 0). apply Qabs_nonneg. intros. rewrite Qabs_neg, Qopp_involutive. apply Qplus_le_l, H. apply (Qplus_le_l _ _ c). ring_simplify. exact (Qle_trans _ _ _ H H0). + intros. apply Qmax_case. intros. apply (Qle_trans _ 0). apply (Qopp_le_compat 0). apply Qabs_nonneg. unfold Qminus. rewrite <- Qle_minus_iff. exact H. intros. setoid_replace (b-c)%Q with (-(c-b)). apply Qopp_le_compat. rewrite Qabs_opp. apply Qle_Qabs. unfold equiv, stdlib_rationals.Q_eq. ring. - apply Qmax_case. + intros. apply Qmax_case. intros. unfold Qminus. rewrite Qplus_opp_r. apply Qabs_nonneg. intros. apply (Qle_trans _ 0). apply (Qplus_le_l _ _ c). ring_simplify. exact H0. apply Qabs_nonneg. + intros. apply Qmax_case. intros. rewrite Qabs_pos. apply Qplus_le_r, Qopp_le_compat, H0. unfold Qminus. rewrite <- Qle_minus_iff. exact (Qle_trans _ _ _ H0 H). intros. apply Qle_Qabs. Qed.
imports: QArith Qabs CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.model.totalorder.QposMinMax CoRN.model.metric2.CRmetric CoRN.model.totalorder.QMinMax CoRN.model.metric2.Qmetric CoRN.metric2.ProductMetric CoRN.stdlib_omissions.Pair MathClasses.interfaces.canonical_names