proposition: Lemma porbit_actperm (a : aT) : a \in D -> porbit (actperm to a) =1 orbit to <[a]>.
proof: Proof. move=> Da x. by rewrite porbitE -orbit_morphim_actperm ?cycle_subG ?morphim_cycle. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)