[PVS-Help] What's the next step to prove it?

[lingzhao <maolzh@xxxxxxxxx>]

I am newer to pvs, when I try to prove some tccs,but I get stuck. The
problem is as follows. So how can I prove it? thanks.

{-1}  x < N
  |-------
{1}   -1 - N * floor((x - 1) / N) + x < N
rule?