proposition: Lemma acts_orbit G x : G \subset D -> [acts G, on orbit to G x | to].
proof: Proof. move/subsetP=> sGD; apply/subsetP=> a Ga; rewrite !inE sGD //. apply/subsetP=> _ /imsetP[b Gb ->]. by rewrite inE -actMin ?sGD // imset_f ?groupM. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)