rw [Nat.add_comm 0]
α : Type u
inst✝¹ : LinearLT α
inst✝ : DecidableRel LT.lt
deg : α → Nat
a : α
n : valType
xs : KVChain LT.lt fun x => valType
haxs : KVChain.boundLeft a xs
⊢ List.foldl (fun c x => c + deg x.fst * x.snd.val) (0 + deg a * n.val) xs.toList =
    deg a * n.val + List.foldl (fun c x => c + deg x.fst * x.snd.val) 0 xs.toList
α : Type u
inst✝¹ : LinearLT α
inst✝ : DecidableRel LT.lt
deg : α → Nat
a : α
n : valType
xs : KVChain LT.lt fun x => valType
haxs : KVChain.boundLeft a xs
⊢ List.foldl (fun c x => c + deg x.fst * x.snd.val) (deg a * n.val + 0) xs.toList =
    deg a * n.val + List.foldl (fun c x => c + deg x.fst * x.snd.val) 0 xs.toList