proposition: Lemma orbit_in_trans G : G \subset D -> transitive (orbit_rel G).
proof: Proof. move=> sGD _ _ z /imsetP[a Ga ->] /imsetP[b Gb ->]. by rewrite -actMin ?mem_orbit ?groupM // (subsetP sGD). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)