m n : ℤ
hne : m ≠ n
⊢ 1 ≤ dist m n
⊢ Pairwise fun m n => 1 ≤ dist m n
intro m n hne
m n : ℤ
hne : m ≠ n
⊢ 1 ≤ abs (↑m - ↑n)
m n : ℤ
hne : m ≠ n
⊢ 1 ≤ dist m n
rw [dist_eq]
m n : ℤ
hne : m ≠ n
⊢ 1 ≤ abs (m - n)
m n : ℤ
hne : m ≠ n
⊢ 1 ≤ abs (↑m - ↑n)
norm_cast
no goals
m n : ℤ
hne : m ≠ n
⊢ 1 ≤ abs (m - n)
rwa [← zero_add (1 : ℤ), Int.add_one_le_iff, abs_pos, sub_ne_zero]