proposition: Lemma plength1_Frattini : K * 'N_G(S) = G.
proof: Proof. rewrite -{2}(Frattini_arg _ sylS_Gp'p) ?pseries_normal //= -plength1_Sylow_prod. by rewrite -mulgA [S * _]mulSGid // subsetI sSG normG. 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)