proposition: Lemma edist_finP (xy : X * X) : (edist xy \is a fin_num)%E <-> exists2 r, 0 < r & ball xy.1 r xy.2.
proof: Proof. rewrite ge0_fin_numE ?edist_ge0// ltey. rewrite -(rwP (negPP eqP)); apply/iff_not2; rewrite notE. apply: (iff_trans (edist_pinftyP _)); apply: (iff_trans _ (forall2NP _ _)). by under eq_forall => ? do rewrite implyE. 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