a : ℤ
a0 : abs a < 1
hn : -1 < a
hp : a < 1
⊢ a = 0
a : ℤ
a0 : abs a < 1
⊢ a = 0
let ⟨hn, hp⟩ := abs_lt.mp a0
a : ℤ
a0 : abs a < 1
hn : -1 < a
hp✝ : a < 1
hp : a ≤ 0
⊢ a = 0
a : ℤ
a0 : abs a < 1
hn : -1 < a
hp : a < 1
⊢ a = 0
rw [←zero_add 1, lt_add_one_iff] at hp
no goals
a : ℤ
a0 : abs a < 1
hn : -1 < a
hp✝ : a < 1
hp : a ≤ 0
⊢ a = 0
exact hp.antisymm hn