change 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
⊢ sum (a :: (as ++ bs)) = sum (a :: as) + sum bs
α : 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