fact: Definition clone_group G := let: Group _ gP := G return {type of Group for G} -> groupT in fun k => k gP.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype div path tuple bigop prime finset)