proposition: Lemma group_setP A : reflect (1 \in A /\ {in A & A, forall x y, x * y \in A}) (group_set A).
proof: Proof. apply: (iffP andP) => [] [A1 AM]; split=> {A1}//. by move=> x y Ax Ay; apply: (subsetP AM); rewrite mem_mulg. by apply/subsetP=> _ /mulsgP[x y Ax Ay ->]; apply: AM. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype div path tuple bigop prime finset)