proposition: Lemma ball_ex_weak_le : forall (X:MetricSpace) (e d:QposInf) (a b:X), QposInf_le e d -> ball_ex e a b -> ball_ex d a b.
proof: Proof. intros X e d a b Hed Hab. destruct d as [d|]; destruct e as [e|]. eapply (ball_weak_le X). apply Hed. assumption. elim Hed. constructor. assumption. Qed.
imports: CoRN.model.totalorder.QposMinMax CoRN.metric2.Metric CoRN.model.structures.QposInf CoRN.stdlib_omissions.List