proposition: Lemma fnd_filterf f P k : (filterf f P).[? k] = if P k then f.[? k] else None.
proof: Proof. case: fndP => [kff|]; last first. by rewrite in_fset => /nandP [/not_fnd->|/negPf-> //]; rewrite if_same. by have := kff; rewrite in_fset => /andP [kf ->]; rewrite ffunE Some_fnd. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)