proposition: Lemma map_pred1_nseq {A : eqType} : forall (l : seq A) n a, a \notin l -> map (pred1 a) (flatten [seq nseq (n x) x | x <- l]) = nseq (\sum_(i <- l) (n i)) false.
proof: Proof. elim. move=> n0 a Ha /=; by rewrite big_nil. move=> h t IH n0 a. rewrite in_cons negb_or. case/andP => H1 H2 /=. rewrite map_cat IH // (_ : map _ _ = nseq (n0 h) false); last first. by rewrite map_nseq /= -(negbTE H1) eqtype.eq_sym. by rewrite big_cons nseq_add. 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