proposition: Lemma act_reprK : {in rcosets 'C_G[x | to] G, cancel (to x \o repr) (amove to G x)}.
proof: Proof. move=> _ /rcosetsP[a Ga ->] /=; rewrite amove_act ?rcoset_repr //. rewrite -[G :&: _]/(gval _); case: repr_rcosetP => b /setIP[Gb _]. exact: groupM. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)