fact: Definition hemiMetricStrong (e:Q) (A B: X -> Prop) := forall x:X, A x -> forall d:Qpos, {y:X | B y /\ ball (e+ proj1_sig d) x y}.
imports: CoRN.algebra.RSetoid CoRN.logic.Classic CoRN.metric2.Metric CoRN.metric2.Classification Coq.Lists.List Coq.ZArith.ZArith CoRN.model.totalorder.QMinMax CoRN.model.totalorder.QposMinMax