a✝ b✝ : ℤ
n✝ : ℕ
a b : ℤ
H1 : 0 ≤ a
H2✝ : a < abs b
n : ℕ
H2 : a < ↑(natAbs -[n+1])
⊢ a / - -[n+1] = -0
a✝ b✝ : ℤ
n✝ : ℕ
a b : ℤ
H1 : 0 ≤ a
H2✝ : a < abs b
n : ℕ
H2 : a < ↑(natAbs -[n+1])
⊢ -(a / -[n+1]) = -0
rw [← Int.ediv_neg]
no goals
a✝ b✝ : ℤ
n✝ : ℕ
a b : ℤ
H1 : 0 ≤ a
H2✝ : a < abs b
n : ℕ
H2 : a < ↑(natAbs -[n+1])
⊢ a / - -[n+1] = -0
exact ediv_eq_zero_of_lt H1 H2