proposition: Lemma edist_fin r (xy : X * X) : 0 < r -> ball xy.1 r xy.2 -> (edist xy <= r%:E)%E.
proof: Proof. move: r => _/posnumP[r] => ?; rewrite -(ereal_inf1 r%:num%:E) le_ereal_inf //. by move=> ? -> /=; exists r%:num; split. 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