fact: Definition Zgroup (gT : finGroupType) (A : {set gT}) := [forall (V : {group gT} | Sylow A V), cyclic V].
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)