proposition: Lemma orbit_rcoset_in A a x y : A \subset D -> a \in D -> (to y a \in orbit to (A :* a) x) = (y \in orbit to A x).
proof: Proof. move=> sAD Da; rewrite -orbit_inv_in ?mul_subG ?sub1set // invMg. by rewrite invg_set1 orbit_lcoset_in ?inv_subG ?groupV ?actKin ?orbit_inv_in. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)