proposition: Lemma ball_splitl (z x y : M) (e : R) : ball x (e / 2) z -> ball y (e / 2) z -> ball x e y.
proof: Proof. by move=> bxz /ball_sym /(ball_split bxz). Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed