proposition: Lemma indporbit_cymap x : indporbit t (cymap x) = indporbit s x.
proof: Proof. Proof using CM. apply eq_ex_minn => i. rewrite {1}/cymap canporbit_cymap eq_in_porbit porbit_cymapcan. rewrite (fs_homog CM (imset_f _ isT)) -{4}(indporbitP s x) eq_in_porbit. suff -> : porbit s x = porbit s (canporbit s x) by []. by apply/eqP; rewrite eq_porbit_mem; apply: canporbitP. 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