proposition: Lemma num_occ_sum_bool : forall t : seq bool, N(true | t) = \sum_(i <- t) i.
proof: Proof. elim => [|hd tl IH]; first by rewrite big_nil num_occ0. rewrite /num_occ /= -/(N(true | tl)) IH big_cons; by case: hd. Qed.
imports: mathcomp(all_ssreflect fingroup perm zmodp ssralg) ssr_ext f2