case mk.cons =>
  intro a b xvars _ _ heq0
  rw [degree_cons] at heq0
  have : deg a * b.1 > 0 := Nat.mul_pos (hdeg_pos a) b.2
  have : deg a * b.val + degree deg ⟨xvars⟩ > 0 :=
    calc
      0 < deg a * b.val := Nat.mul_pos (hdeg_pos a) b.2
      _ ≤ deg a * b.val + degree deg ⟨xvars⟩ := Nat.le_add_right _ _
  rw [heq0] at this
  cases this
α : Type u
inst✝¹ : LinearLT α
inst✝ : DecidableRel LT.lt
deg : α → Nat
hdeg_pos : autoParam (∀ (a : α), deg a > 0) _auto✝
xvars : KVChain LT.lt fun x => valType
⊢ ∀ (a : α) (b : valType) (xs : KVChain LT.lt fun x => valType) (haxs : KVChain.boundLeft a xs),
    (fun xvars => degree deg { vars := xvars } = 0 → { vars := xvars } = 1) xs →
      (fun xvars => degree deg { vars := xvars } = 0 → { vars := xvars } = 1) (KVChain.cons a b xs haxs)
no goals