proposition: Lemma edist_inf0 a : A a -> edist_inf a = 0%E.
proof: Proof. move=> Aa; apply: le_anti; apply/andP; split; last exact: edist_inf_ge0. by apply: ereal_inf_lb; exists a => //; exact: edist_refl. 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