proposition: Lemma cymapE (U V : finType) (s : {perm U}) (t : {perm V}) (CM1 CM2 : porbits_map s t) : {in porbits s, CM1 =1 CM2} -> cymap CM1 =1 cymap CM2.
proof: Proof. Proof using. move=> Heq x; rewrite /cymap /cymapcan /=. rewrite -Heq; last exact: imset_f. case: pickP => // Habs. exfalso; move: Habs. have:= fs_porbitP CM1 x => /imsetP[y _ ->] /(_ y). by rewrite porbit_id. 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