proposition: Lemma ball_close (x y : M) : close x y = forall eps : {posnum R}, ball x eps%:num y.
proof: Proof. rewrite propeqE; split => [cxy eps|cxy]. have := !! cxy _ (open_nbhs_ball _ (eps%:num/2)%:pos). rewrite closureEonbhs/= meetsC meets_globallyr. move/(_ _ (open_nbhs_ball _ (eps%:num/2)%:pos)) => [z [zx zy]]. by apply: (@ball_splitl z); apply: interior_subset. rewrite closeEnbhs => B A /nbhs_ballP[_/posnumP[e2 e2B]] /nbhs_ballP[_/posnumP[e1 e1A]]. by exists y; split; [apply/e2B|apply/e1A; exact: ballxx]. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed