proposition: Lemma orbit_transl G x y z : y \in orbit to G x -> (y \in orbit to G z) = (x \in orbit to G z).
proof: Proof. exact/orbit_in_transl/subsetT. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)