rw [Moveable, not_not]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
⊢ TuranPartition M ↔ ¬Moveable M
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
⊢ TuranPartition M ↔ Balanced M.t fun i => card (MultiPart.P M i)