proposition: Lemma cymapP x : cymap (s x) = t (cymap x).
proof: Proof. Proof using CM. rewrite /cymap -{3}(expg1 s) cymapcan_perm. have:= fs_homog CM (imset_f (x := x) _ isT); rewrite -porbit_cymapcan. move: (cymapcan x) => y H. apply/eqP; rewrite -permM -expgSr eq_in_porbit {}H. have:= canporbitP s x; rewrite -eq_porbit_mem => /eqP ->. rewrite -eq_in_porbit. rewrite expgSr permM indporbitP. have:= mem_porbit s 1 x; rewrite expg1 -eq_porbit_mem canporbitE => /eqP <-. by rewrite indporbitP. 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