proposition: Lemma isgroupP A : reflect (exists G : groupT, A = G) (group_set A).
proof: Proof. by apply: (iffP idP) => [gA | [[B gB] -> //]]; exists (Group gA). Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype div path tuple bigop prime finset)