fact: Definition mkfactors (G : {group gT}) (s : seq {group gT}) := map section_repr (pairmap (@mkSec _) G s).
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype bigop finset fingroup morphism) mathcomp(automorphism quotient action gseries)