proposition: Lemma orbit_in_eqP G x y : G \subset D -> reflect (orbit to G x = orbit to G y) (x \in orbit to G y).
proof: Proof. move=> sGD; apply: (iffP idP) => [yGx|<-]; last exact: orbit_refl. by apply/setP=> z; apply/idP/idP=> /orbit_in_trans-> //; rewrite orbit_in_sym. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)