proposition: Lemma near_covering_withinP (K : set X) : near_covering_within K <-> near_covering K.
proof: Proof. split => cvrW I F P FF cvr; near=> i; (suff: K `<=` fun q : X => K q -> P i q by move=> + k Kk; exact); near: i. by apply: cvrW => x /cvr; apply: filter_app; near=> j. have := cvrW _ _ (fun i q => K q -> P i q) FF. by apply => x /cvr; apply: filter_app; near=> j => + ?; apply. Unshelve. all: by end_near. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed