proposition: Lemma plength1_Sylow_trans (Y : {set gT}) g : Y \subset S -> g \in G -> Y :^ g \subset S -> exists2 c, c \in 'C_G(Y) & exists2 u, u \in 'N_G(S) & g = c * u.
proof: Proof. rewrite -gen_subG -(gen_subG (Y :^ g)) genJ => sYS Gg sYgS. have coKY := coprimegS sYS coKS. have [sYN sYgN] := (subset_trans sYS sSN, subset_trans sYgS sSN). have [c Cc defg] := pprod_trans_coprime defG nsKG sYN coKY solG Gg sYgN. by exists c => //; apply: subsetP Cc; rewrite cent_gen setSI. 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)