proposition: Lemma orbitP A x y : reflect (exists2 a, a \in A & to x a = y) (y \in orbit to A x).
proof: Proof. by apply: (iffP imsetP) => [] [a]; exists a. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)