proposition: Lemma stab_tuple_dprod : 'C[wp | pact] = \big[dprod/1]_(x : seq_sub w) Sym [set i | tnth w i == val x].
proof: Proof. Proof using. rewrite stab_tuple_prod; apply/esym/eqP/bigdprodYP => x /= _. apply/subsetP => /= s; rewrite !inE negb_and negbK => Ht. have {Ht} : s \in Sym [set i | tnth w i != val x]. move: Ht; rewrite bigprodGE => /gen_prodgP[u [/= f Hf ->{s}]]. apply group_prod => j _; move/(_ j): Hf => /bigcupP[k Hk]. rewrite !inE /perm_on => /subset_trans; apply. by apply/subsetP => C; rewrite !inE => /eqP ->. rewrite inE => on_neqi; apply/andP; split. - case: (s =P 1) => //=; apply contra_notN => on_eqi. apply/permP => /= i; rewrite perm1. case: (boolP (tnth w i == val x)) => [HC | /negbTE HC]. + by rewrite (out_perm on_neqi) // !inE HC. + by rewrite (out_perm on_eqi) // !inE HC. - apply/centP => /= u; move: on_neqi. rewrite inE !psupport_perm_on -[psupport u \subset _]setCS => on_neqi on_eqi. apply psupport_disjointC; rewrite disjoints_subset. apply: (subset_trans on_neqi); apply: (subset_trans _ on_eqi). by apply/subsetP => X; rewrite !inE. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup action gproduct) tools combclass sorted partition composition multinomial permcomp cycles