proposition: Lemma gacent_actby B : 'C_(|actby_groupAction)(B) = 'C_(G | to)(A :&: B).
proof: Proof. rewrite /gacent afix_actby !setIA setIid setIUr setICr set0U. by have [nAG sGR] := nGAg; rewrite (setIidPr (acts_dom nAG)) (setIidPl sGR). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)