no goals
ι : Type ?u.161222
α : Type ?u.161225
M : Type ?u.161228
N : Type ?u.161231
P : Type ?u.161234
M₀ : Type ?u.161237
G : Type ?u.161240
R : Type ?u.161243
L : List ℕ
⊢ sum (tail L) = sum L - headI L
rw [← headI_add_tail_sum L, add_comm, @add_tsub_cancel_right]