proposition: Lemma prime_astab (X : finType) (x : X) (c : {perm X}) : prime #|X| -> #[c]%g = #|X| -> 'C_<[c]>[x | 'P]%g = 1%g.
proof: Proof. move=> X_prime ord_c; have /= := card_orbit_stab 'P [group of <[c]>%g] x. rewrite prime_orbit// cardsT [#|<[_]>%g|]ord_c -[RHS]muln1 => /eqP. by rewrite eqn_mul2l gtn_eqF ?prime_gt0//= -trivg_card1 => /eqP. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra all_solvable) mathcomp(all_field)