proposition: Theorem stab_iporbitsE s : stab_iporbits s = \big[dprod/1]_(i < #|T|.+1) Sym (porbits s :&: 'SC_i).
proof: Proof. Proof using. rewrite stab_iporbitsE_prod; apply/esym/eqP/bigdprodYP => i /= _. apply/subsetP => /= t Ht; rewrite !inE negb_and negbK. have {Ht} : t \in Sym (porbits s :&: [set x | #{x} != i]). move: Ht; rewrite bigprodGE => /gen_prodgP[n [/= f Hf ->{t}]]. apply group_prod => j _; move/(_ j): Hf => /bigcupP[k Hk]. rewrite !inE /perm_on => /subset_trans; apply; apply setIS. by apply/subsetP => C; rewrite !inE => /eqP ->. rewrite inE => on_neqi; apply/andP; split. - case: (altP eqP) => //=; apply contra => on_eqi. apply/eqP/permP => C; rewrite perm1. case: (boolP (#|C| == i)) => [HC | /negbTE HC]. + by rewrite (out_perm on_neqi) // !inE HC andbF. + by rewrite (out_perm on_eqi) // !inE HC andbF. - 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 => /andP[ -> ->]. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(tuple path bigop finset div) mathcomp(fingroup perm action gproduct morphism) tools partition permcomp cycles cycletype