proposition: Lemma map_filter_comp (T1 T2: Type) (l : seq T1) (PP : pred T2) (F : T1 -> T2) : [seq F i | i <- l & PP (F i)] = [seq i | i <- map F l & PP i ].
proof: Proof. rewrite filter_map /= -map_comp. have /eq_filter -> : (preim F [eta PP]) =1 (fun i => PP (F i)) by []. by rewrite map_comp. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun ssrnat eqtype fintype choice seq) mathcomp(finset bigop path binomial)