fact: Definition group_valued := forall gT (G : {group gT}), group_set (F G).
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat fintype) mathcomp(bigop finset fingroup morphism automorphism) mathcomp(quotient gproduct)