proposition: Lemma QboundAbs_elim : forall (z:Qpos) (a:Q) (P:Q->Prop), ((proj1_sig z <= a)%Q -> P (proj1_sig z)) -> ((a <= -proj1_sig z)%Q -> P (- proj1_sig z)%Q) -> (QAbsSmall (proj1_sig z) a -> P (a)) -> P (QboundAbs z a).
proof: Proof. intros z a P H1 H2 H3. simpl. apply Qmax_case; apply Qmin_case; intros Z0 Z1; try solve [apply H1;assumption|apply H2;assumption]. elim (Qle_not_lt _ _ Z1). rewrite -> Qlt_minus_iff. ring_simplify. apply (Qpos_ispos ((2#1)*z)). apply H3. split;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