my prove:
we can simple `(n * s) ceildiv a ceildiv s` to `n ceildiv a`
because `(n * s) ceildiv a ceildiv b` <=> `(n * s) ceildiv s ceildiv a`
<=> `n ceildiv a`
let's prove the `s floordiv a floor b` <=> `s floordiv b floor a`
let `s = ka +m (m < a)` so `s floordiv a` <=> `s / a - m / a`
similarly, it can be proven that:
`s floordiv a floordiv b` <=> `s / (a * b) - m / (a * b) - n / (b) constrain (n < b)`
<=> `s / (a * b) - (m + a*n) / (a*b)`
because `a* b - (m + a*n)` <=> `a*b - a*n - m` > `a - m` > `0`
so `s floordiv a floordiv b` <=> `[s / (a*b)]` <=> `s floordiv b floordiv a`
but if `s floordiv b` mutiply a factor above didn't always hold true.
Fixes https://github.com/llvm/llvm-project/issues/107508
51a2f50ee7