proposition: Lemma derivedP G : reflect (exists n, G^`(n) = 1) (solvable G).
proof: Proof. apply: (iffP idP) => [solG | [n solGn]]; last first. apply/forall_inP=> H /subsetIP[sHG sHH']. rewrite -subG1 -{}solGn; elim: n => // n IHn. exact: subset_trans sHH' (commgSS _ _). suffices IHn n: #|G^`(n)| <= (#|G|.-1 - n).+1. by exists #|G|.-1; rewrite [G^`(_)]card_le1_trivg ?(leq_trans (IHn _)) ?subnn. elim: n => [|n IHn]; first by rewrite subn0 prednK. rewrite dergSn subnS -ltnS. have [-> | ntGn] := eqVneq G^`(n) 1; first by rewrite commG1 cards1. case: (_ - _) IHn => [|n']; first by rewrite leqNgt cardG_gt1 ntGn. by apply: leq_trans (proper_card _); apply: sol_der1_proper (der_sub _ _) _. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(fintype div bigop prime finset fingroup morphism) mathcomp(automorphism quotient commutator gproduct) mathcomp(gfunctor center gseries cyclic)