proposition: Lemma domf_filterf f (P : pred K) : domf (filterf f P) = [fset k in domf f | P k].
proof: Proof. by []. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)