proposition: Lemma ball_ex_dec : forall (X:MetricSpace), (forall e (a b:X), {ball e a b}+{~ball e a b}) -> forall e (a b:X), {ball_ex e a b}+{~ball_ex e a b}.
proof: Proof. intros X ball_dec e a b. destruct e as [e|]. apply (ball_dec (proj1_sig e) a b). simpl. auto. Defined.
imports: CoRN.model.totalorder.QposMinMax CoRN.metric2.Metric CoRN.model.structures.QposInf CoRN.stdlib_omissions.List