proposition: Lemma entourageE_subproof A : ent A -> exists2 B, ent B & B \; B `<=` A.
proof: Proof. rewrite entourageE; move=> [_/posnumP[e] sbeA]. exists [set xy | ball xy.1 (e%:num / 2) xy.2]. by exists (e%:num / 2) => /=. move=> xy [z xzhe zyhe]; apply: sbeA. by rewrite [e%:num]splitr; apply: ball_triangle zyhe. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed