proposition: Lemma afix_actby B : 'Fix_<[nRA]>(B) = ~: R :|: 'Fix_to(A :&: B).
proof: Proof. apply/setP=> x; rewrite !inE /= /actby. case: (x \in R); last by apply/subsetP=> a _ /[!inE]. apply/subsetP/subsetP=> [cBx a | cABx a Ba] /[!inE]. by case/andP=> Aa /cBx; rewrite inE Aa. by case: ifP => //= Aa; have:= cABx a; rewrite !inE Aa => ->. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)