proposition: Lemma map_filter_pred1_nseq {A : eqType} (a : A) : forall lst n, uniq lst -> a \in lst -> flatten (map (filter (pred1 a)) (map (fun x => nseq (n x) x) lst)) = nseq (n a) a.
proof: Proof. elim=> // h t IH n0 /=. case/andP=> H1 H2. rewrite in_cons. case/orP. move/eqP => ?; subst a. rewrite {IH} map_filter_nseq_nil //; last first. move=> x0 x0_t /=. apply/eqP => ?; subst x0. by rewrite x0_t in H1. rewrite (_ : filter _ _ = filter xpredT (nseq (n0 h) h)); last first. apply eq_in_filter => i /nseqP[-> /= ]; by rewrite eqxx. by rewrite filter_predT /= cats0. move=> a_t. rewrite IH // (_ : filter _ _ = filter xpred0 (nseq (n0 h) h)); last first. apply eq_in_filter => i /nseqP[-> /= _]. by apply: contraNF H1 => /eqP ->. by rewrite filter_pred0. 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