proposition: Lemma entourage_filter_subproof : Filter ent.
proof: Proof. rewrite entourageE; apply: filter_from_filter; first by exists 1 => /=. move=> _ _ /posnumP[e1] /posnumP[e2]; exists (Num.min e1 e2)%:num => //=. by rewrite subsetI; split=> ?; apply: ball_le; rewrite num_le// le_minl lexx ?orbT. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed