proposition: Lemma distm_lt_splitr (z x y : V) (e : R) : `|z - x| < e / 2 -> `|z - y| < e / 2 -> `|x - y| < e.
proof: Proof. by have := @ball_splitr _ _ z x y e; rewrite -ball_normE. 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