proposition: Lemma subset_closure_half (R : realFieldType) (V : pseudoMetricType R) (x : V) (r : R) : 0 < r -> closed_ball x (r / 2) `<=` ball x r.
proof: Proof. move:r => _/posnumP[r] z /(_ (ball z ((r%:num/2)%:pos)%:num)) []. exact: nbhsx_ballx. by move=> y [+/ball_sym]; rewrite [t in ball x t z]splitr; apply: ball_triangle. 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