rw [turanPartition_iff_not_moveable]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
t : ℕ
M : MultiPart α
hu : M.A = univ
ht : M.t = t
⊢ TuranPartition M → card (edgeFinset (mp M)) = turanNumb t (Fintype.card α)
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
t : ℕ
M : MultiPart α
hu : M.A = univ
ht : M.t = t
⊢ ¬Moveable M → card (edgeFinset (mp M)) = turanNumb t (Fintype.card α)