proposition: Lemma Sylow_gen G : <<\bigcup_(P : {group gT} | Sylow G P) P>> = G.
proof: Proof. set T := [set P : {group gT} | Sylow G P]. rewrite -{2}(@Sylow_transversal_gen T G) => [|P | q _]. - by congr <<_>>; apply: eq_bigl => P; rewrite inE. - by rewrite inE => /and3P[]. by case: (Sylow_exists q G) => P sylP; exists P; rewrite // inE (p_Sylow sylP). 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)