rw [nil_eq_one, one_mul, degree_one]
α : Type u
inst✝³ : LinearLT α
inst✝² : DecidableRel LT.lt
deg : α → Nat
inst✝¹ : LinearLT α
inst✝ : DecidableRel LT.lt
xvars yvars x✝ : KVChain LT.lt fun x => valType
⊢ degree deg ({ vars := KVChain.nil } * { vars := x✝ }) = degree deg { vars := KVChain.nil } + degree deg { vars := x✝ }
α : Type u
inst✝³ : LinearLT α
inst✝² : DecidableRel LT.lt
deg : α → Nat
inst✝¹ : LinearLT α
inst✝ : DecidableRel LT.lt
xvars yvars x✝ : KVChain LT.lt fun x => valType
⊢ degree deg { vars := x✝ } = 0 + degree deg { vars := x✝ }