proposition: Lemma edist_fin_closed : closed [set xy : X * X | edist xy \is a fin_num].
proof: Proof. move=> z /= /(_ (ball z 1)) []; first exact: nbhsx_ballx. move=> w [/edist_finP [] _/posnumP[r] babr [bz1w1 bz2w2]]; apply/edist_finP. exists (1 + (r%:num + 1)) => //. exact/(ball_triangle bz1w1)/(ball_triangle babr)/ball_sym. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrint ssrnum finmap matrix) mathcomp(rat interval zmodp vector fieldext falgebra) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality set_interval Rstruct) ereal reals signed topology prodnormedzmodule