proposition: Lemma ucBall_e_wd : forall (e1 e2:Q) x y, e1 == e2 -> (ucBall e1 x y <-> ucBall e2 x y).
proof: Proof. intros. unfold ucBall in *. split. - intros H0. destruct H0. split. rewrite <- H. exact H0. intro a. apply (ball_e_wd _ _ _ H), H1. - intros. destruct H0. split. rewrite H. exact H0. intro a. apply (ball_e_wd _ _ _ H), H1. Qed.
imports: CoRN.model.totalorder.QposMinMax CoRN.metric2.Metric CoRN.model.structures.QposInf CoRN.stdlib_omissions.List