proposition: Lemma amove_act a : a \in G -> amove to G x (to x a) = 'C_G[x | to] :* a.
proof: Proof. move=> Ga; apply/setP=> b; have Da := ssGD Ga. rewrite mem_rcoset !(inE, sub1set) !groupMr ?groupV //. by case Gb: (b \in G); rewrite //= actMin ?groupV ?ssGD ?(canF_eq (actKVin Da)). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)