proposition: Lemma card_orbit1 G x : #|orbit to G x| = 1%N -> orbit to G x = [set x].
proof: Proof. move=> orb1; apply/eqP; rewrite eq_sym eqEcard {}orb1 cards1. by rewrite sub1set orbit_refl. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)