proposition: Lemma QboundAbs_abs : forall (z:Qpos) (a:Q), Qabs (QboundAbs z a) == Qmin (Qabs a) (proj1_sig z).
proof: Proof. intros. apply QboundAbs_elim. - intros. symmetry. rewrite Qabs_pos, Qabs_pos. apply Qle_min_r, H. apply Qpos_nonneg. apply (Qle_trans _ (`z)). apply Qpos_nonneg. exact H. - intros. symmetry. rewrite Qabs_opp. rewrite (Qabs_pos (`z)). apply Qle_min_r. rewrite Qabs_neg, <- Qopp_involutive. apply Qopp_le_compat, H. apply (Qle_trans _ _ _ H). apply (Qopp_le_compat 0), Qpos_nonneg. apply Qpos_nonneg. - intros. symmetry. apply Qle_min_l. apply AbsSmall_Qabs in H. exact H. 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