fact: Definition maxgroup A gP := maxset (fun A => group_set A && gP <<A>>%G) A.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype div path tuple bigop prime finset)