proposition: Lemma porbits_of_set C : #|C| > 1 -> C \in porbits (perm_of_porbit C).
proof: Proof. Proof using. case: (set_0Vmem C) => [->|]; first by rewrite cards0. move=> [x Hx] Hsize. apply /imsetP; exists (head x (enum C)) => //. exact: perm_of_porbitE. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice fintype) mathcomp(tuple finfun finset path bigop) mathcomp(fingroup perm action) mathcomp(ssralg matrix mxalgebra algC classfun) partition tools sorted permcomp fibered_set cycles