i j : ℕ
h : i < j
⊢ dist i j = max i j - min i j
i j : ℕ
⊢ i < j → dist i j = max i j - min i j
intro h
no goals
i j : ℕ
h : i < j
⊢ dist i j = max i j - min i j
rw [max_eq_right_of_lt h, min_eq_left_of_lt h, dist_eq_sub_of_le (Nat.le_of_lt h)]
i j : ℕ
h : i ≥ j
⊢ dist i j = max i j - min i j
i j : ℕ
⊢ i ≥ j → dist i j = max i j - min i j
intro h
no goals
i j : ℕ
h : i ≥ j
⊢ dist i j = max i j - min i j
rw [max_eq_left h, min_eq_right h, dist_eq_sub_of_le_right h]