proposition: Lemma canporbit_cymap x : canporbit t (cymap x) = cymapcan x.
proof: Proof. Proof using CM. rewrite /cymap /cymapcan /canporbit porbit_perm. have:= erefl (cymapcan x); rewrite {1}/cymapcan. case: pickP => [im Him /= Hdefim | Habs] /=. - rewrite /canporbit (_ : [pick y in _] = some im) //. rewrite [LHS](_ : _ = [pick y in CM (porbit s x)]); first last. apply eq_pick => y /=; congr (y \in _). have:= fs_porbitP x => /imsetP[y0 _ Hy0]. by move: Him; rewrite Hy0 /= -eq_porbit_mem => /eqP ->. rewrite Hdefim /cymapcan. by case: pickP => // /(_ im); rewrite Him. - exfalso; move: Habs. have:= fs_porbitP 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