∀[n:{2...}]. ∀[i:ℤ].  i ÷ n ~ 0 supposing |i| < n
{ Auto }
1. n : {2...}
2. i : ℤ
3. |i| < n
⊢ (i ÷ n) = 0 ∈ ℤ