proposition: Lemma group_setT : group_set (setTfor gT).
proof: Proof. by apply/group_setP; split=> [|x y _ _]; rewrite inE. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype div path tuple bigop prime finset)