proposition: Lemma orbit_in_sym G : G \subset D -> symmetric (orbit_rel G).
proof: Proof. move=> sGD; apply: symmetric_from_pre => x y /imsetP[a Ga]. by move/(canLR (actKin (subsetP sGD a Ga))) <-; rewrite mem_orbit ?groupV. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)