urem x, n: result < n (remainder is always less than divisor) urem x, n: result <= x (remainder is at most the dividend) udiv x, n: result <= x (quotient is at most the dividend) https://alive2.llvm.org/ce/z/ezzsjQ
Decomposition
sub nsw
trunc nsw/nuw
0fdf9b9676