a b : ℤ
m n : ℕ
Ha : -[m+1] < 0
Hb : 0 < ↑(Nat.succ n)
⊢ ediv -[m+1] ↑(Nat.succ n) = -((↑m + 1 - 1) / ↑(Nat.succ n) + 1)
a b : ℤ
m n : ℕ
Ha : -[m+1] < 0
Hb : 0 < ↑(Nat.succ n)
⊢ ediv -[m+1] ↑(Nat.succ n) = -((- -[m+1] - 1) / ↑(Nat.succ n) + 1)
rw [show (- -[m+1] : ℤ) = (m + 1 : ℤ) by rfl]
a b : ℤ
m n : ℕ
Ha : -[m+1] < 0
Hb : 0 < ↑(Nat.succ n)
⊢ ediv -[m+1] ↑(Nat.succ n) = -(↑m / ↑(Nat.succ n) + 1)
a b : ℤ
m n : ℕ
Ha : -[m+1] < 0
Hb : 0 < ↑(Nat.succ n)
⊢ ediv -[m+1] ↑(Nat.succ n) = -((↑m + 1 - 1) / ↑(Nat.succ n) + 1)
rw [add_sub_cancel]
no goals
a b : ℤ
m n : ℕ
Ha : -[m+1] < 0
Hb : 0 < ↑(Nat.succ n)
⊢ ediv -[m+1] ↑(Nat.succ n) = -(↑m / ↑(Nat.succ n) + 1)
rfl
no goals
a b : ℤ
m n : ℕ
Ha : -[m+1] < 0
Hb : 0 < ↑(Nat.succ n)
⊢ - -[m+1] = ↑m + 1
rfl