proposition: Theorem conj_permP s t : reflect (exists c, t = (s ^ c)%g) (cycle_type s == cycle_type t).
proof: Proof. Proof using. apply (iffP eqP) => [/(congr1 val)/= eqct | [x ->]]. - have conjbij_inj := can_inj (conjbijK eqct). exists (perm conjbij_inj); rewrite -permP => x. rewrite !permM permE /= conjbijP. by rewrite -/(conjbij eqct) -(permE conjbij_inj) permKV. - by rewrite cycle_type_conjg. 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