apply Nat.ne_of_lt
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
hu : M.A = univ
h : ¬TuranPartition M
⊢ ¬card (edgeFinset (mp M)) = turanNumb M.t (Fintype.card α)
case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
hu : M.A = univ
h : ¬TuranPartition M
⊢ card (edgeFinset (mp M)) < turanNumb M.t (Fintype.card α)