proposition: Lemma num_occ_perm (a : A) (s : 'S_n) : N(a | perm_tuple s t) = N(a | t).
proof: Proof. rewrite 2!num_occ_alt. rewrite (_ : set_occ a (perm_tuple s t) = s^-1 @: set_occ a t). apply/card_imset/perm_inj. apply/eqP. rewrite eqEsubset. apply/andP; split; apply/subsetP => i. - rewrite in_set => H. apply/imsetP. exists (s i); last by rewrite -permM mulgV perm1. rewrite in_set. move/eqP : H => <-; by rewrite /perm_tuple tnth_map tnth_ord_tuple. - rewrite in_set. case/imsetP => j. rewrite in_set. move/eqP => <- ->. by rewrite tnth_map tnth_ord_tuple permKV. Qed.
imports: mathcomp(all_ssreflect fingroup perm zmodp ssralg) ssr_ext f2