proposition: Lemma card_orbit_in_stab G x : G \subset D -> (#|orbit to G x| * #|'C_G[x | to]|)%N = #|G|.
proof: Proof. by move=> sGD; rewrite mulnC card_orbit_in ?Lagrange ?subsetIl. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)