proposition: Lemma pgroup_sol p P : p.-group P -> solvable P.
proof: Proof. by move/pgroup_nil; apply: nilpotent_sol. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(fintype prime bigop finset fingroup morphism) mathcomp(automorphism quotient action cyclic gproduct) mathcomp(gfunctor commutator pgroup center nilpotent)