[Aardwolf]

Very well written and informative!

One random thing I wonder: in the lexicographic ordering, is there any reason why the convention is that x_2 < x_1, while x^2 > x^1? Where _ denotes subscript, ^ superscript exponents, in other words that x > y uses opposite of alphabetic ordering, while the exponents are done in non-opposite numeric order? I don't think the naming of the variables matters for the mathematical result (you can use any subscript or letter for any variable as long as the corresponding ones remain the same between the equations), so the convention x_1 < x_2 would work just as well, and be less confusing I think.

[ransac9000]

This is a good point. I think it's just due to convention --- people tend to put terms involving x only at the front, and in the textbook by Cox et. al. that I referenced they use this convention as well.

[wizzwizz4]

I find x₁ > x₂ for lexicographic ordering less confusing, because it works like the dictionary.