∀ {u v : Lean.Level} {M : Q(Type v)} {R : Q(Type u)} (iR : Q(Ring «$R»)) (x x_1 : Mathlib.Tactic.Module.qNF R M),
  Mathlib.Tactic.Module.qNF.sub iR x x_1 =
    match x, x_1 with
    | [], l => l.onScalar q(Neg.neg)
    | l, [] => l
    | ((a₁, x₁), k₁) :: t₁, ((a₂, x₂), k₂) :: t₂ =>
      if k₁ < k₂ then ((a₁, x₁), k₁) ::ᵣ Mathlib.Tactic.Module.qNF.sub iR t₁ (((a₂, x₂), k₂) ::ᵣ t₂)
      else
        if k₁ = k₂ then ((q(«$a₁» - «$a₂»), x₁), k₁) ::ᵣ Mathlib.Tactic.Module.qNF.sub iR t₁ t₂
        else ((q(-«$a₂»), x₂), k₂) ::ᵣ Mathlib.Tactic.Module.qNF.sub iR (((a₁, x₁), k₁) ::ᵣ t₁) t₂