Lean4
/-- Given a product of powers, split as a quotient: the positive powers divided by (the negations
of) the negative powers. -/
def split (iM : Q(CommGroupWithZero $M)) (l : qNF M) :
MetaM (Σ l_n l_d : qNF M, Q(NF.eval $(l.toNF) = NF.eval $(l_n.toNF) / NF.eval $(l_d.toNF))) := do
match l with
| [] =>
return ⟨[], [], q(Eq.symm (div_one (1 : $M)))⟩
| ((r, x), i) :: t =>
let ⟨t_n, t_d, pf⟩ ← split iM t
if r > 0 then
return ⟨((r, x), i) :: t_n, t_d, (q(NF.cons_eq_div_of_eq_div $r $x $pf) :)⟩
else if r = 0 then
return ⟨((1, x), i) :: t_n, ((1, x), i) :: t_d, (q(NF.cons_zero_eq_div_of_eq_div $x $pf) :)⟩
else
let r' : ℤ := -r
return ⟨t_n, ((r', x), i) :: t_d, (q(NF.cons_eq_div_of_eq_div' $r' $x $pf) :)⟩
