proposition: Lemma Frattini_arg H P : G <| H -> p.-Sylow(G) P -> G * 'N_H(P) = H.
proof: Proof. case/andP=> sGH nGH sylP; rewrite -normC ?subIset ?nGH ?orbT // -astab1JG. move/subgroup_transitiveP: Syl_trans => ->; rewrite ?inE //. apply/imsetP; exists P; rewrite ?inE //. apply/eqP; rewrite eqEsubset -{1}((atransP Syl_trans) P) ?inE // imsetS //=. by apply/subsetP=> _ /imsetP[x Hx ->]; rewrite inE -(normsP nGH x Hx) pHallJ2. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(fintype prime bigop finset fingroup morphism) mathcomp(automorphism quotient action cyclic gproduct) mathcomp(gfunctor commutator pgroup center nilpotent)