proposition: Lemma asimple_quo_maxainv (G H : {group rT}) : H \subset D -> G \subset D -> [acts A, on G | to] -> [acts A, on H | to] -> H <| G -> asimple (to / H) (G / H) -> maxainv to G H.
proof: Proof. move=> sHD sGD aG aH nHG /asimpleP[ntQ maxQ]; apply/maxgroupP; split. by rewrite nHG -quotient_sub1 ?normal_norm // subG1 ntQ. move=> K /and3P[nKG nsGK aK] sHK. pose K' := (K / H)%G. have K'dQ : K' <| (G / H)%G by apply: morphim_normal. have nKH : H <| K by rewrite (normalS _ _ nHG) // normal_sub. have: K' :=: 1%G \/ K' :=: (G / H). apply: (maxQ K' K'dQ) => /=. apply/subsetP=> x Adx. rewrite inE Adx /= inE. apply/subsetP=> y. rewrite quotientE; case/morphimP=> z Nz Kz ->; rewrite /= !inE qactE //. have ntoyx : to z x \in 'N(H) by rewrite (acts_qact_dom_norm Adx). apply/morphimP; exists (to z x) => //. suff h: qact_dom to H \subset A. by rewrite astabs_act // (subsetP aK) //; apply: (subsetP h). by apply/subsetP=> t; rewrite qact_domE // inE; case/andP. case=> [|/quotient_injG /[!inE]/(_ nKH nHG) c]; last by rewrite c subxx in nsGK. rewrite /= -trivg_quotient => tK'; apply: (congr1 (@gval _)); move: tK'. by apply: (@quotient_injG _ H); rewrite ?inE /= ?normal_refl. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype bigop finset fingroup morphism) mathcomp(automorphism quotient action gseries)