@dwarn Thanks! I couldn't yet connect everything, but using your keyword Dickson's lemma I found it interesting that Cox, Little, O'Shea in their very nice book Ideals, Varieties and Algorithms call Dickson's lemma the statement that every ideal generated by monomials in a polynomial ring over a field is finitely generated. They give a direct proof (not referring to Hilbert's basis theorem), but at first sight it doesn't seem to be fully constructive.

(Btw, there is a recent 5th edition from 2025 of their book, as I just found out.)