Anytime I see questions on mse that ask something “simple”, I feel a powerful urge to chime in with “a computer can do this for you!”. Obviously if you’re a researching mathematician you shouldn’t waste your time with something a computer can do for you, but when you’re still learning techniques (or, as is frequently the case on mse, solving homework problems), it’s not a particularly useful comment (so I usually abstain). The urge is particularly powerful when it comes to the contrived inequalities that show up in a lot of competition math, and today I saw a question that really made me want to say something about this! I still feel like it would be a bit inappropriate for mse, but thankfully I have a blog where I can talk about whatever I please :P So today, let’s see how to hit these problems with the proverbial nuke that is quantifier elimination!