proposition: Lemma orbit_refl G x : x \in orbit to G x.
proof: Proof. by rewrite -{1}[x]act1 mem_orbit. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)