rw [h_ind]
α : Type u
inst✝ : AddMonoid α
bs : List α
a : α
as : List α
h_ind : sum (as ++ bs) = sum as + sum bs
⊢ a + sum (as ++ bs) = a + sum as + sum bs
α : Type u
inst✝ : AddMonoid α
bs : List α
a : α
as : List α
h_ind : sum (as ++ bs) = sum as + sum bs
⊢ a + (sum as + sum bs) = a + sum as + sum bs