proposition: Lemma maxainvM (G H K : {group rT}) : H \subset D -> K \subset D -> maxainv G H -> maxainv G K -> H :<>: K -> H * K = G.
proof: Proof. move: H K => N1 N2 sN1D sN2D pmN1 pmN2 neN12. have cN12 : commute N1 N2. apply: normC; apply: (subset_trans (maxainv_sub pmN1)). by rewrite normal_norm ?maxainv_norm. wlog nsN21 : G N1 N2 sN1D sN2D pmN1 pmN2 neN12 cN12/ ~~(N1 \subset N2). move/eqP: (neN12); rewrite eqEsubset negb_and; case/orP=> ns; first by apply. by rewrite cN12; apply=> //; apply: sym_not_eq. have nP : N1 * N2 <| G by rewrite normalM ?maxainv_norm. have sN2P : N2 \subset N1 * N2 by rewrite mulg_subr ?group1. case/maxgroupP: (pmN1); case/andP=> nN1G pN1G mN1. case/maxgroupP: (pmN2); case/andP=> nN2G pN2G mN2. case/andP: pN1G=> nsGN1 ha1; case/andP: pN2G=> nsGN2 ha2. case e : (G \subset N1 * N2). by apply/eqP; rewrite eqEsubset e mulG_subG !normal_sub. have: N1 <*> N2 = N2 by apply: mN2; rewrite /= ?comm_joingE // nP e /= gactsM. by rewrite comm_joingE // => h; move: nsN21; rewrite -h mulg_subl. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype bigop finset fingroup morphism) mathcomp(automorphism quotient action gseries)