proposition: Lemma stab_iporbitsE_prod s : stab_iporbits s = (\prod_(i < #|T|.+1) Sym_group (porbits s :&: 'SC_i))%G.
proof: Proof. Proof using. apply/setP => t. rewrite inE bigprodGE; apply/andP/idP => [[Ht /bigcapP/(_ _ isT) Hcyi] | Ht]. - rewrite -(perm_decE (s := t) (trivIset_iporbits s)); first last. + apply/astabP => /= CS /imsetP[/= i _ ->{CS}]. by apply/astab1P; rewrite astab1_set; exact: Hcyi. + by move: Ht; rewrite inE -psupport_perm_on cover_iporbits. apply group_prod => u /imsetP[/= X /imsetP[/= i _ ->{X}] ->{u}]. apply mem_gen; apply/bigcupP; exists i; first by []. by rewrite inE; exact: restr_perm_on. split; move: t Ht; apply/subsetP; rewrite gen_subG; apply/subsetP => /= P /bigcupP[/= i _]. - rewrite !inE !psupport_perm_on => /subset_trans; apply. exact: subsetIl. - rewrite inE => HP. apply/bigcapP => /= j _; apply/astabsP => /= X; rewrite apermE. case: (P X =P X) => [-> // | /eqP HPX]. have:= HP => /subsetP/(_ X); rewrite inE => /(_ HPX) H. have:= H; rewrite -(perm_closed _ HP). by move: H; rewrite !inE => /andP[-> /eqP ->] /andP[-> /eqP ->]. 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