proposition: Lemma quo2_plength1 gT p (G H K : {group gT}) : H <| G -> K <| G -> H :&: K = 1 -> p.-length_1 (G / H) && p.-length_1 (G / K) = p.-length_1 G.
proof: Proof. move=> nHG nKG trHK. have [p_pr | p_nonpr] := boolP (prime p); last by rewrite !plength1_nonprime. apply/andP/idP=> [[pH1 pK1] | pG1]; last by rewrite !plength1_quo. pose U := p_elt_gen p G; have nU : U <| G by apply: p_elt_gen_normal. have exB (N : {group gT}) : N <| G -> p.-length_1 (G / N) -> exists B : {group gT}, [/\ U \subset 'N(B), forall x, x \in B -> #[x] = p -> x \in N & forall Q : {group gT}, p^'.-subgroup(U) Q -> Q \subset B]. - move=> nsNG; have [sNG nNG] := andP nsNG. rewrite p_elt_gen_length1 // (_ : p_elt_gen _ _ = U / N); last first. rewrite /quotient morphim_gen -?quotientE //; last first. by rewrite setIdE subIset ?nNG. congr <<_>>; apply/setP=> Nx; rewrite inE setIdE quotientGI // inE. apply: andb_id2l => /morphimP[x NNx Gx ->{Nx}] /=. apply/idP/idP=> [pNx | /morphimP[y NNy]]; last first. by rewrite inE => p_y ->; apply: morph_p_elt. rewrite -(constt_p_elt pNx) -morph_constt // mem_morphim ?groupX //. by rewrite inE p_elt_constt. have nNU: U \subset 'N(N) := subset_trans (normal_sub nU) nNG. have nN_UN: U <*> N \subset 'N(N) by rewrite gen_subG subUset normG nNU. case/(inv_quotientN _): (pcore_normal p^' [group of U <*> N / N]) => /= [|B]. by rewrite /normal sub_gen ?subsetUr. rewrite /= quotientYidr //= /U => defB sNB; case/andP=> sB nB hallB. exists B; split=> [| x Ux p_x | Q /andP[sQU p'Q]]. - by rewrite (subset_trans (sub_gen _) nB) ?subsetUl. - have nNx: x \in 'N(N) by rewrite (subsetP nN_UN) ?(subsetP sB). apply: coset_idr => //; rewrite -[coset N x](consttC p). rewrite !(constt1P _) ?mulg1 // ?p_eltNK. by rewrite morph_p_elt // /p_elt p_x pnat_id. have: coset N x \in B / N by apply/morphimP; exists x. by apply: mem_p_elt; rewrite /= -defB pcore_pgroup. rewrite -(quotientSGK (subset_trans sQU nNU) sNB). by rewrite -defB (sub_Hall_pcore hallB) ?quotientS ?quotient_pgroup. have{pH1} [A [nAU pA p'A]] := exB H nHG pH1. have{pK1 exB} [B [nBU pB p'B]] := exB K nKG pK1. rewrite p_elt_gen_length1 //; apply: normal_max_pgroup_Hall (pcore_normal _ _). apply/maxgroupP; split; first by rewrite /psubgroup pcore_sub pcore_pgroup. move=> Q p'Q sOQ; apply/eqP; rewrite eqEsubset sOQ andbT. apply: subset_trans (_ : U :&: (A :&: B) \subset _); last rewrite /U. by rewrite !subsetI p'A ?p'B //; case/andP: p'Q => ->. apply: pcore_max; last by rewrite /normal subsetIl !normsI ?normG. rewrite /pgroup p'natE //. apply/negP=> /Cauchy[] // x /setIP[_ /setIP[Ax Bx]] oxp. suff: x \in 1%G by move/set1P=> x1; rewrite -oxp x1 order1 in p_pr. by rewrite /= -trHK inE pA ?pB. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq path div fintype) mathcomp(bigop prime binomial finset fingroup morphism perm automorphism) mathcomp(quotient action gproduct gfunctor commutator) mathcomp(ssralg finalg zmodp cyclic center pgroup finmodule gseries) mathcomp(nilpotent sylow abelian maximal hall extremal) mathcomp(matrix mxalgebra mxrepresentation mxabelem)