proposition: Lemma group_set_astabs S : group_set 'N(S | to).
proof: Proof. apply/group_setP; split=> [|a b cSa cSb]. by rewrite !inE group1; apply/subsetP=> x Sx; rewrite inE act1. rewrite !inE groupM ?(@astabs_dom _ _ _ to S) //; apply/subsetP=> x Sx. by rewrite inE actMin ?(@astabs_dom _ _ _ to S) ?astabs_act. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)