proposition: Lemma asimpleP K : reflect [/\ K :!=: 1 & forall H, H <| K -> [acts A, on H | to] -> H :=: 1 \/ H :=: K] (asimple K).
proof: Proof. apply: (iffP idP). case/maxgroupP; rewrite normal1 /=; case/andP=> nsK1 aK H1. rewrite eqEsubset negb_and nsK1 /=; split => // H nHK ha. case eHK : (H :==: K); first by right; apply/eqP. left; apply: H1; rewrite ?sub1G // nHK; move/negbT: eHK. by rewrite eqEsubset negb_and normal_sub //=; move->. case=> ntK h; apply/maxgroupP; split. move: ntK; rewrite eqEsubset sub1G andbT normal1; move->. apply/subsetP=> a Da; rewrite !inE Da /= sub1set !inE. by rewrite /= -actmE // morph1 eqxx. move=> H /andP[nHK /andP[nsKH ha]] _. case: (h _ nHK ha)=> // /eqP; rewrite eqEsubset. by rewrite (negbTE nsKH) andbF. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype bigop finset fingroup morphism) mathcomp(automorphism quotient action gseries)