proposition: Lemma group_set_gacent A : group_set 'C_(|to)(A).
proof: Proof. apply/group_setP; split=> [|x y]. by rewrite !inE group1; apply/subsetP=> a /setIP[Da _]; rewrite inE gact1. case/setIP=> Rx /afixP cAx /setIP[Ry /afixP cAy]. rewrite inE groupM //; apply/afixP=> a Aa. by rewrite gactM ?cAx ?cAy //; case/setIP: Aa. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)