id,summary,reporter,owner,description,type,status,priority,milestone,component,resolution,keywords,cc,merged,author,reviewer,upstream,work_issues,branch,commit,dependencies,stopgaps
22025,minus of real x should be known to be at most abs(x),pelegm,,"Check this:
{{{#!python
sage: assume(x, 'real')
sage: bool(x <= abs(x))
True
}}}
but
{{{#!python
sage: bool(-x <= abs(x))
False
}}}
and even
{{{#!python
sage: bool(-x <= abs(-x))
False
}}}
(so this is a bit inconsistent).
Solve works here, but the set of solutions is not well simplified:
{{{#!python
sage: solve(x <= abs(x), x)
#0: solve_rat_ineq(ineq=_SAGE_VAR_x <= abs(_SAGE_VAR_x))
[[x == 0], [0 < x], [x < 0]]
sage: solve(-x <= abs(x), x)
#0: solve_rat_ineq(ineq=-_SAGE_VAR_x <= abs(_SAGE_VAR_x))
[[x == 0], [x < 0], [0 < x]]
}}}
(so it also gives a debug message; see #22018)
",enhancement,new,major,sage-wishlist,symbolics,,abs,,,,,N/A,,,,,