apply DIV
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
ix bound modulus : ℕ
IX : ix < bound
MODULUS : modulus > 0
DIV : bound % modulus = 0
⊢ 0 < modulus