proposition: Lemma map_filter_nseq_nil {A : eqType} : forall (l : seq A) (p : pred A) n, (forall x, x \in l -> ~~ p x) -> flatten (map (filter p) (map (fun x => nseq (n x) x) l)) = [::].
proof: Proof. elim=> // h t IH p n0 H /=. rewrite IH. - rewrite cats0. transitivity (filter xpred0 (nseq (n0 h) h)). apply eq_in_filter => a /nseqP[-> _]. apply/negP/negP/H; by rewrite in_cons eqxx. by rewrite filter_pred0. move=> x0 Hx0. apply H; by rewrite in_cons Hx0 orbC. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum fingroup perm) Reals mathcomp(Rstruct) ssrR Reals_ext realType_ext ssr_ext ssralg_ext logb fdist entropy num_occ channel types