proposition: Lemma hemiMetric_refl : forall (e:Q) A, 0 <= e -> hemiMetric e A A.
proof: Proof. intros e epos A x Hx. apply existsWeaken. exists x. split; try assumption. apply ball_refl. exact A. Qed.
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