[llvm] [SCEV] BECount to zero if `((-C + (C smax %x)) /u %x), C > 0` holds (PR #104580)

[Antonio Frighetto via llvm-commits]

antoniofrighetto wrote:

> We don't need nsw as a precondition either, it's implied: https://alive2.llvm.org/ce/z/_dLm8C

Generalized and proof updated, thanks.

https://github.com/llvm/llvm-project/pull/104580