proposition: Lemma QboundAbs_absorb: forall (a b:Qpos) (c:Q), proj1_sig a <= proj1_sig b -> QboundAbs b (QboundAbs a c) == QboundAbs a c.
proof: Proof. intros a b c H. simpl. rewrite -> Qmin_max_distr_r. setoid_replace (Qmin (proj1_sig b) (-proj1_sig a)) with (-proj1_sig a). rewrite -> Qmax_assoc. rewrite <- Qmin_max_de_morgan. rewrite -> Qmin_assoc. setoid_replace (Qmin (proj1_sig b) (proj1_sig a)) with (proj1_sig a). reflexivity. rewrite <- Qle_min_r. assumption. rewrite <- Qle_min_r. rewrite -> Qle_minus_iff. ring_simplify. destruct a,b. simpl. rewrite <- (Qplus_0_l 0). apply Qplus_le_compat; apply Qlt_le_weak; assumption. 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