rw [mul_add,add_mul,mul_one,one_mul]
α : Type ?u.138093
inst✝¹ : Fintype α
inst✝ : DecidableEq α
b a n : ℕ
hb : b + 1 < a
hn : a + b ≤ n
⊢ a * (n - a) + b * (n - b) < (a - 1) * (n - a + 1) + (b + 1) * (n - b - 1)
α : Type ?u.138093
inst✝¹ : Fintype α
inst✝ : DecidableEq α
b a n : ℕ
hb : b + 1 < a
hn : a + b ≤ n
⊢ a * (n - a) + b * (n - b) < (a - 1) * (n - a) + (a - 1) + (b * (n - b - 1) + (n - b - 1))