proposition: Lemma simple_sol_prime G : solvable G -> simple G -> prime #|G|.
proof: Proof. move=> solG /simpleP[ntG simG]. have{solG} cGG: abelian G. apply/commG1P; case/simG: (der_normal 1 G) => // /eqP/idPn[]. by rewrite proper_neq // (sol_der1_proper solG). case: (trivgVpdiv G) ntG => [-> | [p p_pr]]; first by rewrite eqxx. case/Cauchy=> // x Gx oxp _; move: p_pr; rewrite -oxp orderE. have: <[x]> <| G by rewrite -sub_abelian_normal ?cycle_subG. by case/simG=> -> //; rewrite cards1. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(div fintype finfun bigop finset prime binomial) mathcomp(fingroup morphism perm automorphism quotient) mathcomp(action commutator gproduct gfunctor ssralg) mathcomp(countalg finalg zmodp cyclic pgroup center gseries) mathcomp(nilpotent sylow abelian finmodule)