proposition: Lemma pprod_focal_coprime : H :&: G^`(1) = H :&: U^`(1).
proof: Proof. set G' := G^`(1); set U' := U^`(1). have [sU'U nU'U] := andP (der_normal 1 U : U' <| U). have{nU'U} nU_U': U :&: _ \subset 'N(U') by move=> A; rewrite subIset ?nU'U. suffices sHG'U': H :&: G' \subset U'. by rewrite -(setIidPl sHG'U') -setIA (setIidPr (dergS 1 sUG)). rewrite -(setIidPr sHU) -setIA -quotient_sub1 // setICA setIC. rewrite quotientGI ?subsetI ?sU'U ?dergS ?coprime_TIg //= -/G' -/U'. have sUG'_UKb: (U :&: G') / U' \subset (U :&: K) / U'. rewrite quotientSK // -normC ?group_modr ?setIS //. by rewrite -quotientSK ?comm_subG ?quotient_der // -defG quotientMidl. rewrite (coprimeSg sUG'_UKb) // -(card_isog (second_isog _)) //=. rewrite setIA (setIidPl sU'U) coprime_morphl ?coprime_morphr //. exact: coprimeSg (subsetIr U K) coKH. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq div fintype finset) mathcomp(prime fingroup morphism automorphism quotient gproduct gfunctor) mathcomp(cyclic center commutator pgroup nilpotent sylow abelian hall) mathcomp(maximal) odd_order(BGsection1 BGappendixAB)