Lean4
/-- Given two terms `l₁`, `l₂` of type `qNF M`, i.e. lists of `(ℤ × Q($M)) × ℕ`s (an integer, an
`Expr` and a natural number), construct another such term `l`, which will have the property that in
the field `$M`, the quotient of the "multiplicative linear combinations" represented by `l₁` and
`l₂` is the multiplicative linear combination represented by `l`.
The construction assumes, to be valid, that the lists `l₁` and `l₂` are in strictly decreasing order
by `ℕ`-component, and that if pairs `(a₁, x₁)` and `(a₂, x₂)` appear in `l₁`, `l₂` respectively with
the same `ℕ`-component `k`, then the expressions `x₁` and `x₂` are equal.
The construction is as follows: merge the first list and the negation of the second list, except
that if pairs `(a₁, x₁)` and `(a₂, x₂)` appear in `l₁`, `l₂` respectively with the same
`ℕ`-component `k`, then contribute a term `(a₁ - a₂, x₁)` to the output list with `ℕ`-component `k`.
-/
def div : qNF M → qNF M → qNF M
| [], l => l.onExponent Neg.neg
| l, [] => l
| ((a₁, x₁), k₁) :: t₁, ((a₂, x₂), k₂) :: t₂ =>
if k₁ > k₂ then ((a₁, x₁), k₁) :: div t₁ (((a₂, x₂), k₂) :: t₂)
else if k₁ = k₂ then ((a₁ - a₂, x₁), k₁) :: div t₁ t₂ else ((-a₂, x₂), k₂) :: div (((a₁, x₁), k₁) :: t₁) t₂
