Simplify symbolic equation based on assumptions?

edit

Hi guys,

I'm using Sage since few days ago. I'm struggling solving some inequalities with constraints.

I have two questions that may be related.

First, why do we obtain such result in the following code?

var('x, y')
assume(x, 'real', y, 'real')
assume(x>0, y>0)
assume(x-y < 0)
bool(x-y < 0) # => True
bool(x-y < 1) # => False

Second, when I compute some equation, I obtain a result with a square root of something that I know is negative. So I make some assumption on that value and I obtain the result I expect.

var('x, y')
assume(x>0, y>0)
assume(x-y<0)

sqrt(x-y).real().simplify_full() # => 0
sqrt(x-y).imag().simplify_full() # => sqrt(-x+y)

Then, if I want to compute another square root that should also be negative using the previous assumption. Sage does not simplify the equation.

sqrt(x-y-1).real().simplify_full() # => sqrt(abs(-x + y + 1))*cos(1/2*arctan2(0, x - y - 1))
sqrt(x-y-1).imag().simplify_full() # => sqrt(abs(-x + y + 1))*sin(1/2*arctan2(0, x - y - 1))

Then I have to explicitely set another assumption (which is less restrictive by the say) to obtain the result I want. I this the wanted behavior?

assume(x-y-1<0)

sqrt(x-y-1).real().simplify_full() # => 0
sqrt(x-y-1).imag().simplify_full() # => sqrt(-x + y + 1)

My full problem is the following:

var('s, a, g, xi, w0, w')

assume(a, 'real', g, 'real', xi, 'real', w0, 'real', w, 'real') # Real variables
assume(a>0, g>0, xi>0, w0>0, w>0) # Positive variables
assume(xi<1/sqrt(2))

G = g/(s^2/w0^2 + 2*xi*s/w0 + 1);
Gv_cst = g/a;

assume(a>1)

s1 = (G + Gv_cst).roots(s)

I want to show that the roots have a negative real part. I tried many things but with no succes. Here is one of my trials:

s1[0][0].real().is_negative()

Thank you very much.