proposition: Lemma orbit_lcoset_in A a x : A \subset D -> a \in D -> orbit to (a *: A) x = orbit to A (to x a).
proof: Proof. move/subsetP=> sAD Da; apply/setP=> y; apply/imsetP/imsetP=> [] [b Ab ->{y}]. by exists (a^-1 * b); rewrite -?actMin ?mulKVg // ?sAD -?mem_lcoset. by exists (a * b); rewrite ?mem_mulg ?set11 ?actMin // sAD. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)