proposition: Lemma group_setI G H : group_set (G :&: H).
proof: Proof. apply/group_setP; split=> [|x y]; rewrite !inE ?group1 //. by case/andP=> Gx Hx; rewrite !groupMl. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype div path tuple bigop prime finset)