x -nsw y < -C is false when x > y and C >= 0 Alive2 proof for sgt, sge : https://alive2.llvm.org/ce/z/tupvfi Note: It only really makes sense in the context of signed comparison for "X - Y must be positive if X >= Y and no overflow". Fixes https://github.com/llvm/llvm-project/issues/54735
x-y+1 is positive when x > y, so abs (x-y+1) --> x-y+1 Fixes https://github.com/llvm/llvm-project/issues/54735