proposition: Lemma orbit_inv_in A x y : A \subset D -> (y \in orbit to A^-1 x) = (x \in orbit to A y).
proof: Proof. move/subsetP=> sAD; apply/imsetP/imsetP=> [] [a Aa ->]. by exists a^-1; rewrite -?mem_invg ?actKin // -groupV sAD -?mem_invg. by exists a^-1; rewrite ?memV_invg ?actKin // sAD. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)