proposition: Theorem cent1_permE s : 'C[s] = 'CC(s) ><| (permcycles s) @* (stab_iporbits s).
proof: Proof. Proof using. apply/esym/sdprod_normal_complP. - apply/normalP; split; first exact: subsetIl. move=> /= y Hy; apply/setP => /= x; have /= HyV := groupVr Hy. apply/imsetP/idP => [[/= z Hz] ->{x} | Hx]. + exact: conj_porbitgrp. + exists (x ^ (y^-1)); last by rewrite conjgKV. exact: conj_porbitgrp. rewrite /= -/(stab_iporbits s). rewrite inE; apply/andP; split. - apply/eqP/trivgP; apply/subsetP => t. rewrite 2!inE => /andP[/imsetP[/= P]]. rewrite setIid => HP Ht /andP[tC tCporbits]; rewrite inE. suff : P = 1 by rewrite Ht => ->; rewrite morphism.morph1. by rewrite -(permcyclesK HP) -Ht; apply: inporbits1. - rewrite /=; apply/eqP/setP => /= t. apply/idP/idP => [/mulsgP[/= t' u /imsetP[P]] | Ht]. + rewrite setIid => HP ->{t'} Hu ->{t}. apply groupM; first exact: permcyclesP. by move: Hu; rewrite inE => /andP[]. + exact: (subsetP (cent1_stab_iporbit_porbitgrpS s)). 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