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