proposition: Lemma amove_orbit : amove to G x @: orbit to G x = rcosets 'C_G[x | to] G.
proof: Proof. apply/setP => Ha; apply/imsetP/rcosetsP=> [[y] | [a Ga ->]]. by case/imsetP=> b Gb -> ->{Ha y}; exists b => //; rewrite amove_act. by rewrite -amove_act //; exists (to x a); first apply: mem_orbit. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)