i j : ℕ
hne : i ≠ j
h : i < j
⊢ 0 < j - i
i j : ℕ
hne : i ≠ j
h : i < j
⊢ 0 < dist i j
rw [dist_eq_sub_of_le (le_of_lt h)]
no goals
i j : ℕ
hne : i ≠ j
h : i < j
⊢ 0 < j - i
apply tsub_pos_of_lt h
no goals
i j : ℕ
hne : i ≠ j
h : i = j
⊢ 0 < dist i j
contradiction
i j : ℕ
hne : i ≠ j
h : i > j
⊢ 0 < i - j
i j : ℕ
hne : i ≠ j
h : i > j
⊢ 0 < dist i j
rw [dist_eq_sub_of_le_right (le_of_lt h)]
no goals
i j : ℕ
hne : i ≠ j
h : i > j
⊢ 0 < i - j
apply tsub_pos_of_lt h