proposition: Lemma edist_triangle (x y z : X) : (edist (x, z) <= edist (x, y) + edist (y, z))%E.
proof: Proof. have [->|] := eqVneq (edist (x, y)) +oo%E; first by rewrite addye ?leey. have [->|] := eqVneq (edist (y, z)) +oo%E; first by rewrite addey ?leey. rewrite -?ltey -?ge0_fin_numE//. move=> /edist_finP [_/posnumP[r2] /= yz] /edist_finP [_/posnumP[r1] /= xy]. have [|] := eqVneq (edist (x, z)) +oo%E. move/edist_pinftyP /(_ (r1%:num + r2%:num) _) => -[//|]. exact: (ball_triangle xy). rewrite -ltey -ge0_fin_numE// => /[dup] xzfin. move/edist_finP => [_/posnumP[del] /= xz]. rewrite /edist /= ?ereal_inf_EFin; first last. - by exists (r1%:num + r2%:num); split => //; apply: (ball_triangle xy). - by exists 0 => ? /= [/ltW]. - by exists r1%:num; split. - by exists 0 => ? /= [/ltW]. - by exists r2%:num; split. - by exists 0 => ? /= [/ltW]. rewrite -EFinD lee_fin -inf_sumE //; first last. - by split; [exists r2%:num; split| exists 0 => ? /= [/ltW]]. - by split; [exists r1%:num; split| exists 0 => ? /= [/ltW]]. apply: lb_le_inf. by exists (r1%:num + r2%:num); exists r1%:num => //; exists r2%:num. move=> ? [+ []] => _/posnumP[p] xpy [+ []] => _/posnumP[q] yqz <-. apply: inf_lb; first by exists 0 => ? /= [/ltW]. by split => //; apply: (ball_triangle xpy). 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