∀[a,n:ℕ].  (a ÷ n) = 0 ∈ ℤ supposing a < n
{ (UnivCD THENA Auto) }
1. a : ℕ
2. n : ℕ
3. a < n
⊢ (a ÷ n) = 0 ∈ ℤ