proposition: Lemma cymapcan_perm i x : cymapcan ((s ^+ i)%g x) = cymapcan x.
proof: Proof. Proof using CM. rewrite /cymapcan porbit_perm. have:= fs_porbitP x => /imsetP[y0 _ ->]. by case: pickP => // /(_ y0); 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