proposition: Lemma QboundAbs_contract : forall (c : Qpos) (j k : Q), Qabs (QboundAbs c j - QboundAbs c k) <= Qabs (j-k).
proof: Proof. intros. apply QboundAbs_elim. - intros. apply QboundAbs_elim. + intros. unfold Qminus. rewrite Qplus_opp_r. apply Qabs_nonneg. + intros. unfold Qminus. rewrite Qopp_involutive. rewrite Qabs_pos, Qabs_pos. apply Qplus_le_compat. exact H. rewrite <- Qopp_involutive. apply Qopp_le_compat. exact H0. apply (Qle_trans _ (`c + `c)). apply (Qpos_nonneg (c+c)). apply Qplus_le_compat. exact H. rewrite <- Qopp_involutive. apply Qopp_le_compat. exact H0. apply (Qpos_nonneg (c+c)). + intros [H0 H1]. rewrite Qabs_pos. 2: unfold Qminus; rewrite <- Qle_minus_iff; exact H1. apply (Qle_trans _ (j-k)). apply Qplus_le_l. exact H. apply Qle_Qabs. - intros. apply QboundAbs_elim. + intros. setoid_replace (- `c - `c) with (-(`c+`c)) by (unfold equiv, stdlib_rationals.Q_eq; ring). rewrite Qabs_opp. rewrite Qabs_pos. 2: apply (Qpos_nonneg (c+c)). rewrite Qabs_Qminus. rewrite Qabs_pos. apply Qplus_le_compat. exact H0. rewrite <- Qopp_involutive. apply Qopp_le_compat. exact H. apply (Qle_trans _ (`c + `c)). apply (Qpos_nonneg (c+c)). apply Qplus_le_compat. exact H0. rewrite <- Qopp_involutive. apply Qopp_le_compat. exact H. + intros. unfold Qminus. rewrite Qopp_involutive, Qplus_comm, Qplus_opp_r. apply Qabs_nonneg. + intros [H0 H1]. setoid_replace (- `c - k) with (-(`c+k)) by (unfold equiv, stdlib_rationals.Q_eq; ring). rewrite Qabs_opp. rewrite Qabs_pos, Qabs_Qminus. apply (Qle_trans _ (k-j)). rewrite Qplus_comm. apply Qplus_le_r. rewrite <- Qopp_involutive. apply Qopp_le_compat. exact H. apply Qle_Qabs. apply (Qplus_le_l _ _ (-`c)). ring_simplify. ring_simplify in H0. exact H0. - intros [H0 H1]. apply QboundAbs_elim. + intros. rewrite Qabs_Qminus, Qabs_pos. rewrite Qabs_Qminus, Qabs_pos. apply Qplus_le_l, H. unfold Qminus. rewrite <- Qle_minus_iff. exact (Qle_trans _ _ _ H1 H). unfold Qminus. rewrite <- Qle_minus_iff. exact H1. + intros. unfold Qminus. rewrite Qopp_involutive, Qabs_pos. apply (Qle_trans _ (j-k)). apply Qplus_le_r. rewrite <- Qopp_involutive. apply Qopp_le_compat. exact H. apply Qle_Qabs. apply (Qplus_le_l _ _ (`c)) in H0. ring_simplify in H0. rewrite Qplus_comm. exact H0. + intros [H2 H3]. apply Qle_refl. Qed.
imports: CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.model.totalorder.QposMinMax CoRN.model.lattice.CRlattice CoRN.model.totalorder.QMinMax Coq.QArith.Qabs CoRN.model.metric2.Qmetric CoRN.metric2.ProductMetric MathClasses.interfaces.canonical_names