A monomial ordering is a total order on ℕ^r making ℕ^r into an ordered monoid, i.e. 0 <= m for all m and m <= m' implies m + n <= m' + n for all m, m', n.

Classically, every monomial ordering is a well-ordering (algebra people like to deduce this from Hilbert's basis theorem).

Is it true constructively that every monomial ordering is well-founded, i.e. allows well-founded induction?

Feel free to boost if you have constructive people in your bubble 😅