rw [Nat.add_assoc]
case H
α : 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
x✝ : Nat
y✝ : (_ : α) × valType
⊢ deg a * n.val + x✝ + deg y✝.fst * y✝.snd.val = deg a * n.val + (x✝ + deg y✝.fst * y✝.snd.val)
no goals