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), recursively construct a proof that in the field `$M`, the quotient
of the "multiplicative linear combinations" represented by `l₁` and `l₂` is the multiplicative
linear combination represented by `FieldSimp.qNF.div l₁ l₁`. -/
def mkDivProof (iM : Q(CommGroupWithZero $M)) (l₁ l₂ : qNF M) :
Q(NF.eval $(l₁.toNF) / NF.eval $(l₂.toNF) = NF.eval $((qNF.div l₁ l₂).toNF)) :=
match l₁, l₂ with
| [], l => (q(NF.one_div_eq_eval $(l.toNF)) :)
| l, [] => (q(div_one (NF.eval $(l.toNF))) :)
| ((a₁, x₁), k₁) :: t₁, ((a₂, x₂), k₂) :: t₂ =>
if k₁ > k₂ then
let pf := mkDivProof iM t₁ (((a₂, x₂), k₂) :: t₂)
(q(NF.div_eq_eval₁ ($a₁, $x₁) $pf) :)
else
if k₁ = k₂ then
let pf := mkDivProof iM t₁ t₂
(q(NF.div_eq_eval₂ $a₁ $a₂ $x₁ $pf) :)
else
let pf := mkDivProof iM (((a₁, x₁), k₁) :: t₁) t₂
(q(NF.div_eq_eval₃ ($a₂, $x₂) $pf) :)
