proposition: Lemma hemiMetric_stable :forall e A B, ~~(hemiMetric e A B) -> hemiMetric e A B.
proof: Proof. unfold hemiMetric. auto 7 using existsC_stable. 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