proposition: Lemma amoveK : {in orbit to G x, cancel (amove to G x) (fun Ca => to x (repr Ca))}.
proof: Proof. move=> _ /orbitP[a Ga <-]; rewrite amove_act //= -[G :&: _]/(gval _). case: repr_rcosetP => b; rewrite !(inE, sub1set)=> /and3P[Gb _ xbx]. by rewrite actMin ?ssGD ?(eqP xbx). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)