proposition: Lemma partnCTE p1 p2 : (p1 == p2) = (partnCT p1 == partnCT p2).
proof: Proof. Proof using. rewrite /partnCT. apply/eqP/eqP => [-> //|]. case: p1 p2 => [p1 Hp1] [p2 Hp2]. move/(congr1 val); rewrite !cast_intpartnE /= => Hp. exact: val_inj. 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