[PVS-Help] inequalities in PVS

[A Serebrenik <aserebre@xxxxxxxxxx>]

Dear all,

I wonder what proof command should I use for simple manipulation of 
inequalities? I would like, e.g. to prove the following sequent:
{-1}  integer_pred(x!1)
{-2}  x!1 < 1000
{-3}  x!1 > 1
{-4}  x!1 * x!1 > 1
{-5}  x!1 * x!1 < 1000
   |-------
{1}   1000 - x!1 * x!1 < 1000 - x!1

Using (both-sides - 1000) and (assert) I can reduce the succedent to
{1'}  -1 * (x!1 * x!1) < -1 * x!1 but this is as far as I get: (both-sides 
* -1) results in an unexpected:
{1''}  -1 * (x!1 * x!1) * -1 < -1 * x!1 * -1

Best regards,
Alexander Serebrenik