proposition: Lemma cast_cycle_typeSN m n (s : 'S_m) (eq_mn : m = n) : cycle_typeSn (cast_perm eq_mn s) = cast_intpartn eq_mn (cycle_typeSn s).
proof: Proof. by subst n. 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