[SCEV] Prove condition invariance via context, try 2

Initial implementation had too weak requirements to positive/negative
range crossings. Not crossing zero with nuw is not enough for two reasons:

- If ArLHS has negative step, it may turn from positive to negative
  without crossing 0 boundary from left to right (and crossing right to
  left doesn't count for unsigned);
- If ArLHS crosses SINT_MAX boundary, it still turns from positive to
  negative;

In fact we require that ArLHS always stays non-negative or negative,
which an be enforced by the following set of preconditions:

- both nuw and nsw;
- positive step (looks liftable);

Because of positive step, boundary crossing is only possible from left
part to the right part. And because of no-wrap flags, it is guaranteed
to never happen.