proposition: Lemma hemiMetricStrong_refl : forall (e:Q) A, 0 <= e -> hemiMetricStrong e A A.
proof: Proof. intros e A epos x Hx d. exists x. split; try assumption. apply ball_refl. apply (Qle_trans _ (e+0)). rewrite Qplus_0_r. exact epos. apply Qplus_le_r. apply (Qpos_nonneg d). 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