rewrite [Nat.div_lt_iff_lt_mul, Nat.mul_cancel_right]
ix bound modulus : ℕ
IX : ix < bound
MODULUS : modulus > 0
DIV : bound % modulus = 0
⊢ ix / modulus < bound / modulus
ix bound modulus : ℕ
IX : ix < bound
MODULUS : modulus > 0
DIV : bound % modulus = 0
⊢ ix < bound

case MODZERO
ix bound modulus : ℕ
IX : ix < bound
MODULUS : modulus > 0
DIV : bound % modulus = 0
⊢ bound % modulus = 0

ix bound modulus : ℕ
IX : ix < bound
MODULUS : modulus > 0
DIV : bound % modulus = 0
⊢ 0 < modulus