proposition: Lemma mem_filterf f (P : pred K) (k : K) : (k \in domf (filterf f P)) = (k \in f) && (P k) :> bool.
proof: Proof. by rewrite !inE. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)