proposition: Lemma maxainv_asimple_quo (G H : {group rT}) : H \subset D -> maxainv to G H -> asimple (to / H) (G / H).
proof: Proof. move=> sHD /maxgroupP[/and3P[nHG pHG aH] Hmax]. apply/asimpleP; split; first by rewrite -subG1 quotient_sub1 ?normal_norm. move=> K' nK'Q aK'. have: (K' \proper (G / H)) || (G / H == K'). by rewrite properE eqEsubset andbC (normal_sub nK'Q) !andbT orbC orbN. case/orP=> [ pHQ | eQH]; last by right; apply sym_eq; apply/eqP. left; pose K := ((coset H) @*^-1 K')%G. have eK'I : K' \subset (coset H) @* 'N(H). by rewrite (subset_trans (normal_sub nK'Q)) ?morphimS ?normal_norm. have eKK' : K' :=: K / H by rewrite /(K / H) morphpreK //=. suff eKH : K :=: H by rewrite -trivg_quotient eKK' eKH. have sHK : H \subset K by rewrite -ker_coset kerE morphpreS // sub1set group1. apply: Hmax => //; apply/and3P; split; last exact: qacts_cosetpre. by rewrite -(quotientGK nHG) cosetpre_normal. by move: (proper_subn pHQ); rewrite sub_morphim_pre ?normal_norm. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype bigop finset fingroup morphism) mathcomp(automorphism quotient action gseries)