theorem Hex.Perm.Cycle.split_ones (xs : List ℕ) (hp : ∀ x ∈ xs, 0 < x) : ↑xs = ↑(List.filter (fun (x : ℕ) => decide (1 < x)) xs) + Multiset.replicate (List.count 1 xs) 1

theorem Hex.Perm.cycleType_eq_mathlib {n : ℕ} (p : Perm n) : ↑p.cycleType.toList = Equiv.Perm.cycleType p.toEquiv + Multiset.replicate (n - (Equiv.Perm.support p.toEquiv).card) 1

The complete executable cycle type is Mathlib's nontrivial cycle type with one entry for each fixed point.

theorem Hex.Perm.cycleType_conj {n : ℕ} (p q : Perm n) : ((q.comp p).comp q.inv).cycleType = p.cycleType

Conjugation preserves the sorted cycle type, including fixed points.