rw [add_mul, mul_assoc, Nat.add_mul_div_left _ _ (Nat.succ_pos n)]
n d : ℕ
inst✝ : NeZero d
w : Weight n d
k : ℕ
⊢ (∑ x : Fin (n + 1), w x + (n + 1) * k) * d / (n + 1) + 1 = (∑ x : Fin (n + 1), w x) * d / (n + 1) + 1 + k * d
n d : ℕ
inst✝ : NeZero d
w : Weight n d
k : ℕ
⊢ (∑ x : Fin (n + 1), w x) * d / Nat.succ n + k * d + 1 = (∑ x : Fin (n + 1), w x) * d / (n + 1) + 1 + k * d