proposition: Lemma num_occ_sum : forall (t : seq 'F_2), num_occ 1%R t = \sum_(i <- t) i.
proof: Proof. elim => [ /= | /= h t ->]; first by rewrite big_nil. rewrite big_cons; by case/F2P: h. Qed.
imports: mathcomp(all_ssreflect fingroup perm zmodp ssralg) ssr_ext f2