# [PVS-Help] Looking for general strategy to solve inequality problem

 Hi all,I have the following statement, which [-1]  dx < -140[-2]  dv < 50  |-------[1]   dx < -150[2]   dv < 45[3]   (1 + (dv - 50 + dv * ((140 + dx) / 10) - 50 * ((140 + dx) / 10)) / 5 + (140 + dx) / 10)       / 1       >=       122957620769739151/5000000000000000000 * dx - 475345081090927124023/100000000000000000000 + 10091024637222290039/100000000000000000000 * dvLeaving the original as-is and doing (field 3) results in:{-1}  100000000000000000000 > 0{-2}  dx < -140{-3}  dv < 50  |-------{1}   dx < -150{2}   dv < 45{3}   500000000000000000000 +       (20000000000000000000 * (dv * dx) + 2800000000000000000000 * dv) / 10       - (140000000000000000000000 + 1000000000000000000000 * dx) / 10       + 20000000000000000000 * dv       + 10000000000000000000 * dx       >=       (10091024637222290039 * dv) - 475345081090927124023 + 2459152415394783020 * dxI manually figured out that  [3] can also be simplified to:   (dx + 150) * (dv - 45) / 50 >=        122957620769739151/5000000000000000000 * dx - 475345081090927124023/100000000000000000000 + 10091024637222290039/100000000000000000000 * dvUsing a case-replace and field I end up with:{-1}  100000000000000000000 > 0{-2}  (1 + (140 + dx) / 10 +        (-50 - 50 * ((140 + dx) / 10) + (140 + dx) / 10 * dv + dv) / 5)       / 1       = (dx + 150) * (dv - 45) / 50{-3}  dx < -140{-4}  dv < 50  |-------{1}   dx < -150{2}   dv < 45{3}   2000000000000000000 * ((dv - 45) * (dx + 150)) >=       (10091024637222290039 * dv) - 475345081090927124023 +        2459152415394783020 * dxThis still wasn’t very helpful, so I used Wolfram-Alpha to simplify the inequality and got:(2000000000000000000 * dv - 92459152415394783020) * dx >= 13024654918909072875977 - 289908975362777709961 * dvUsing a case-replace and field I end up with:{-1}  2000000000000000000 * ((dv - 45) * (dx + 150)) >=       (10091024637222290039 * dv) - 475345081090927124023 +        2459152415394783020 * dx       =       (2000000000000000000 * dv - 92459152415394783020) * dx >=        13024654918909072875977 - 289908975362777709961 * dv{-2}  100000000000000000000 > 0{-3}  (1 + (140 + dx) / 10 +        (-50 - 50 * ((140 + dx) / 10) + (140 + dx) / 10 * dv + dv) / 5)       / 1       = (dx + 150) * (dv - 45) / 50{-4}  dx < -140{-5}  dv < 50  |-------{1}   dx < -150{2}   dv < 45{3}   (2000000000000000000 * dv - 92459152415394783020) * dx >=       13024654918909072875977 - 289908975362777709961 * dvNow, I imagine I could probably solve this eventually (I’ve already graphed it to prove to myself that it’s true), but I was wondering if there’s a better strategy I could be using in general?Best Regards,Ben Hockingbenjaminhocking@xxxxxxxxx