proposition: Lemma orbit_sym G x y : (x \in orbit to G y) = (y \in orbit to G x).
proof: Proof. exact/orbit_in_sym/subsetT. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)