proposition: Lemma Sylow_transversal_gen (T : {set {group gT}}) G : (forall P, P \in T -> P \subset G) -> (forall p, p \in \pi(G) -> exists2 P, P \in T & p.-Sylow(G) P) -> << \bigcup_(P in T) P >> = G.
proof: Proof. move=> G_T T_G; apply/eqP; rewrite eqEcard gen_subG. apply/andP; split; first exact/bigcupsP. apply: dvdn_leq (cardG_gt0 _) _; apply/dvdn_partP=> // q /T_G[P T_P sylP]. by rewrite -(card_Hall sylP); apply: cardSg; rewrite sub_gen // bigcup_sup. 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)