proposition: Lemma exists_comps (G : gTg) : exists s, comps G s.
proof: Proof. elim: {G} #|G| {1 3}G (leqnn #|G|) => [G | n IHn G cG]. by rewrite leqNgt cardG_gt0. have [sG | nsG] := boolP (simple G). by exists [:: 1%G]; rewrite /comps eqxx /= -simple_maxnormal andbT. have [-> | ntG] := eqVneq G 1%G; first by exists [::]; rewrite /comps eqxx. have [N maxN] := ex_maxnormal_ntrivg ntG. have [|s /andP[ls cs]] := IHn N. by rewrite -ltnS (leq_trans _ cG) // proper_card // (maxnormal_proper maxN). by exists (N :: s); apply/and3P. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype bigop finset fingroup morphism) mathcomp(automorphism quotient action gseries)