proposition: Lemma orbit_in_transl G x y z : G \subset D -> y \in orbit to G x -> (y \in orbit to G z) = (x \in orbit to G z).
proof: Proof. by move=> sGD Gxy; rewrite !(orbit_in_sym sGD _ z) (orbit_in_eqP y x sGD Gxy). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)