proposition: Lemma rfd_iso : 'C_('Alt_T)[x | 'P] \isog 'Alt_T'.
proof: Proof. have rgd_x p: rgd p x = x by rewrite permE /= insubF //= eqxx. have rfd_rgd p: rfd (rgd p) = p. apply/permP => [[z Hz]]; apply/val_eqP; rewrite !permE. by rewrite /= [rgd _ _]permE /= insubF eqxx // permE /= insubT. have sSd: 'C_('Alt_T)[x | 'P] \subset 'dom rfd. by apply/subsetP=> p /[!inE]/= /andP[]. apply/isogP; exists [morphism of restrm sSd rfd] => /=; last first. rewrite morphim_restrm setIid; apply/setP=> z; apply/morphimP/idP=> [[p _]|]. case/setIP; rewrite Alt_even => Hp; move/astab1P=> Hp1 ->. by rewrite Alt_even rfd_odd. have dz': rgd z x == x by rewrite rgd_x. move=> kz; exists (rgd z); last by rewrite /= rfd_rgd. by rewrite 2!inE (sameP astab1P eqP). rewrite 4!inE /= (sameP astab1P eqP) dz' -rfd_odd; last exact/eqP. by rewrite rfd_rgd mker // ?set11. apply/injmP=> x1 y1 /=. case/setIP=> Hax1; move/astab1P; rewrite /= /aperm => Hx1. case/setIP=> Hay1; move/astab1P; rewrite /= /aperm => Hy1 Hr. apply/permP => z. case (z =P x) => [->|]; [by rewrite Hx1 | move/eqP => nzx]. move: (congr1 (fun q : {perm T'} => q (Sub z nzx)) Hr). by rewrite !permE => [[]]; rewrite Hx1 Hy1 !eqxx. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(div fintype tuple tuple bigop prime finset fingroup) mathcomp(morphism perm automorphism quotient action cyclic) mathcomp(pgroup gseries sylow primitive_action)