proposition: Lemma asimple_acompsP K s : acomps K s -> reflect (s = [:: 1%G]) (asimple K).
proof: Proof. move=> cs; apply: (iffP idP); last first. by move=> se; move: cs; rewrite se /=; case/andP=> /=; rewrite andbT. case: s cs. by rewrite /acomps /= andbT; move/eqP->; case/asimpleP; rewrite eqxx. move=> H s cs sG; apply/eqP. rewrite eqseq_cons -(trivg_acomps (acomps_cons cs)) andbC andbb. case/acompsP: cs => /= ls; case/andP=> mH ps. case/maxgroupP: sG; case/and3P => _ ntG _ ->; rewrite ?sub1G //. rewrite (maxainv_norm mH); case/andP: (maxainv_proper mH)=> _ ->. exact: (maxainv_ainvar mH). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype bigop finset fingroup morphism) mathcomp(automorphism quotient action gseries)