proposition: Lemma prime_orbit (X : finType) x c : prime #|X| -> #[c]%g = #|X| -> orbit 'P <[c]> x = [set: X].
proof: Proof. move=> X_prime ord_c; have dvd_orbit y : (#|orbit 'P <[c]> y| %| #|X|)%N. by rewrite (dvdn_trans (dvdn_orbit _ _ _))// [#|<[_]>%g|]ord_c. have [] := boolP [forall y, #|orbit 'P <[c]> y| == 1%N]. move=> /'forall_eqP-/(_ _)/card_orbit1 orbit1; suff c_eq_1 : c = 1%g. by rewrite c_eq_1 ?order1 in ord_c; rewrite -ord_c in X_prime. apply/permP => y; rewrite perm1. suff: c y \in orbit 'P <[c]> y by rewrite orbit1 inE => /eqP->. by apply/orbitP; exists c => //; rewrite mem_gen ?inE. move=> /forallPn[y orbit_y_neq0]; have orbit_y : orbit 'P <[c]> y = [set: X]. apply/eqP; rewrite eqEcard subsetT cardsT. by have /(prime_nt_dvdP X_prime orbit_y_neq0)<-/= := dvd_orbit y. by have /orbit_in_eqP-> : x \in orbit 'P <[c]> y; rewrite ?subsetT ?orbit_y. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra all_solvable) mathcomp(all_field)