proposition: Lemma edist_inf_triangle x y : (edist_inf x <= edist (x, y) + edist_inf y)%E.
proof: Proof. have [A0|/set0P[a0 Aa0]] := eqVneq A set0. by rewrite /edist_inf A0 ?image_set0 ?ereal_inf0 addey. have [fyn|] := boolP (edist_inf y \is a fin_num); first last. by rewrite ge0_fin_numE// ?ltey negbK => /eqP->; rewrite addey ?leey. have [xyfin|] := boolP (edist (x, y) \is a fin_num); first last. by rewrite ge0_fin_numE// ?ltey // negbK => /eqP->; rewrite addye ?leey. apply/lee_addgt0Pr => _/posnumP[eps]. have [//|? [a Aa <-] yaeps] := @lb_ereal_inf_adherent R _ eps%:num _ fyn. apply: le_trans; first by apply: (@ereal_inf_lb _ _ (edist (x, a))); exists a. apply: le_trans; first exact: (@edist_triangle _ _ _ y). by rewrite -addeA leeD2lE // ltW. 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