# Long but easy inequality fails to simplify - where did I go wrong?

Trying to create a simple example I find I need a number of variables.

All my variables are Reals and greater 0. So I use

$Assumptions = Element[lab, Reals] && Element[q, Reals] && Element[r, Reals] && Element[s, Reals] && Element[t, Reals] && Element[u, Reals] && Element[v, Reals] && lab > 0 && q > 0 && r > 0 && s > 0 && t > 0 && u > 0 && v > 0 && q < 1  From an equation system I get lengthy solutions having terms like following and I am interested whether they are smaller 0. My problem is to weed out the parts that are "obviously" true. So I actually obtain the following expressions as part of a larger expression. (s (-1 + q - q u)) < 0 // Refine lab (-1 + q) q u v < 0 // Refine  They instantly evaluate to True But as things get more complex (here just summing the two expressions) - Simplify (or Refine) fail to find the simplification instantly (in the sense that they immediately give up). (s (-1 + q - q u)) + lab (-1 + q) q u v < 0 // Refine  I found just if would delete the lab it would evaluate nicely. But since I have many much longer expressions this is not really an option to weed through the sub expressions manually. All this calculations happen instantaneously and I could definitely live with Mathematica spending some minutes searching for this simplifications. So I am very open to any suggestions even if they strain my machine a bit. Update After a few days I also wrote to community.wolfram.com. A user there suggested to use Simplify[Equivalent[$Assumptions, Reduce[\$Assumptions && (s (-1 + q - q u)) + lab (-1 + q) q u v < 0]]] - which seems to do what I want.

I am not putting it as answer yet as I still am curious why Simplify doesn't catch this trivial case.

• Note that #>0 implies Reals – Feyre Dec 19 '16 at 13:44
• Thanks that will shorten my code - I just wanted to assure I had all conditions spelled out. – bdecaf Dec 19 '16 at 13:46
• For those looking at this question, there are definitely some weird things going on here... Looking at the last code line provided in the OP, there's aq*u*v in the right term. If you take away u the Refine doesn't transform the expression, but if you remove the v instead it does: Refine[(s (-1 + q - q u)) + lab (-1 + q) q v < 0] gives True. More generally, you can remove the letter if it doesn't appear in the left term, so Refine[(s (-1 + q - q v)) + lab (-1 + q) q v < 0] does compute. Thus Mathematica seems to need some sort of factorization to be able to transform it. – Musang Dec 19 '16 at 15:36
• Can use FindInstance on the reversed inequality to show it cannot be satisfied: FindInstance[(s (-1 + q - q u)) + lab (-1 + q) q u v >= 0 && lab > 0 && q > 0 && r > 0 && s > 0 && t > 0 && u > 0 && v > 0 && q < 1, {s, q, u, lab, v, r, s, t}] Out[464]= {} – Daniel Lichtblau Dec 23 '16 at 18:45
• It seems i didn't clearly explain - i'm having a more complex expression - imagine (u-v) multiplied with one of the terms above. And I am after a simplification to (u-v)>0 - if there is any. – bdecaf Dec 25 '16 at 21:45

To show this, cast it as a quantifier elimination problem and let Resolve do what its name implies.

Resolve[
Exists[{s, q, u, lab, v, r, s, t},
lab > 0 && q > 0 && r > 0 && s > 0 && t > 0 && u > 0 && v > 0 &&
q < 1, (s (-1 + q - q u)) + lab (-1 + q) q u v < 0]]

(* Out[466]= True *)
`
• Interesting. I didn't know about resolve. I will try it when i get back to the lab. – bdecaf Dec 25 '16 at 21:51