proposition: Lemma orbit_conjsg_in A a x y : A \subset D -> a \in D -> (to y a \in orbit to (A :^ a) (to x a)) = (y \in orbit to A x).
proof: Proof. move=> sAD Da; rewrite conjsgE. by rewrite orbit_lcoset_in ?groupV ?mul_subG ?sub1set ?actKin ?orbit_rcoset_in. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)