proposition: Lemma exists_acomps K : exists s, acomps K s.
proof: Proof. elim: {K} #|K| {1 3}K (leqnn #|K|) => [K | n Hi K cK]. by rewrite leqNgt cardG_gt0. case/orP: (orbN (asimple K)) => [sK | nsK]. by exists [:: (1%G : {group rT})]; rewrite /acomps eqxx /= andbT. case/orP: (orbN (K :==: 1))=> [tK | ntK]. by exists (Nil _); rewrite /acomps /= andbT. case: (maxainv_exists ntK)=> N pmN. have cN: #|N| <= n. by rewrite -ltnS (leq_trans _ cK) // proper_card // (maxainv_proper pmN). case: (Hi _ cN)=> s; case/andP=> lasts ps; exists [:: N & s]; rewrite /acomps. by rewrite last_cons lasts /= pmN. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype bigop finset fingroup morphism) mathcomp(automorphism quotient action gseries)