[GOAL]
n m : ℕ
⊢ dist n m = dist m n
[PROOFSTEP]
simp [dist.def, add_comm]
[GOAL]
n : ℕ
⊢ dist n n = 0
[PROOFSTEP]
simp [dist.def, tsub_self]
[GOAL]
n m : ℕ
h : n = m
⊢ dist n m = 0
[PROOFSTEP]
rw [h, dist_self]
[GOAL]
n m : ℕ
h : n ≤ m
⊢ dist n m = m - n
[PROOFSTEP]
rw [dist.def, tsub_eq_zero_iff_le.mpr h, zero_add]
[GOAL]
n m : ℕ
h : m ≤ n
⊢ dist n m = n - m
[PROOFSTEP]
rw [dist_comm]
[GOAL]
n m : ℕ
h : m ≤ n
⊢ dist m n = n - m
[PROOFSTEP]
apply dist_eq_sub_of_le h
[GOAL]
n m : ℕ
⊢ m ≤ n + dist n m
[PROOFSTEP]
rw [add_comm]
[GOAL]
n m : ℕ
⊢ m ≤ dist n m + n
[PROOFSTEP]
apply dist_tri_left
[GOAL]
n m : ℕ
⊢ n ≤ dist n m + m
[PROOFSTEP]
rw [dist_comm]
[GOAL]
n m : ℕ
⊢ n ≤ dist m n + m
[PROOFSTEP]
apply dist_tri_left
[GOAL]
n m : ℕ
⊢ n ≤ m + dist n m
[PROOFSTEP]
rw [dist_comm]
[GOAL]
n m : ℕ
⊢ n ≤ m + dist m n
[PROOFSTEP]
apply dist_tri_right
[GOAL]
n k m : ℕ
⊢ n + k - (m + k) + (m + k - (n + k)) = n - m + (m + k - (n + k))
[PROOFSTEP]
rw [@add_tsub_add_eq_tsub_right]
[GOAL]
n k m : ℕ
⊢ n - m + (m + k - (n + k)) = n - m + (m - n)
[PROOFSTEP]
rw [@add_tsub_add_eq_tsub_right]
[GOAL]
k n m : ℕ
⊢ dist (k + n) (k + m) = dist n m
[PROOFSTEP]
rw [add_comm k n, add_comm k m]
[GOAL]
k n m : ℕ
⊢ dist (n + k) (m + k) = dist n m
[PROOFSTEP]
apply dist_add_add_right
[GOAL]
n m k l : ℕ
h : n + m = k + l
⊢ dist n k = dist (n + m) (k + m)
[PROOFSTEP]
rw [dist_add_add_right]
[GOAL]
n m k l : ℕ
h : n + m = k + l
⊢ dist (n + m) (k + m) = dist (k + l) (k + m)
[PROOFSTEP]
rw [h]
[GOAL]
n m k l : ℕ
h : n + m = k + l
⊢ dist (k + l) (k + m) = dist l m
[PROOFSTEP]
rw [dist_add_add_left]
[GOAL]
n m k : ℕ
⊢ dist n k ≤ dist n m + dist m k
[PROOFSTEP]
have : dist n m + dist m k = n - m + (m - k) + (k - m + (m - n)) := by
  simp [dist.def, add_comm, add_left_comm, add_assoc]
[GOAL]
n m k : ℕ
⊢ dist n m + dist m k = n - m + (m - k) + (k - m + (m - n))
[PROOFSTEP]
simp [dist.def, add_comm, add_left_comm, add_assoc]
[GOAL]
n m k : ℕ
this : dist n m + dist m k = n - m + (m - k) + (k - m + (m - n))
⊢ dist n k ≤ dist n m + dist m k
[PROOFSTEP]
rw [this, dist.def]
[GOAL]
n m k : ℕ
this : dist n m + dist m k = n - m + (m - k) + (k - m + (m - n))
⊢ n - k + (k - n) ≤ n - m + (m - k) + (k - m + (m - n))
[PROOFSTEP]
exact add_le_add tsub_le_tsub_add_tsub tsub_le_tsub_add_tsub
[GOAL]
n k m : ℕ
⊢ dist (n * k) (m * k) = dist n m * k
[PROOFSTEP]
rw [dist.def, dist.def, right_distrib, tsub_mul n, tsub_mul m]
[GOAL]
k n m : ℕ
⊢ dist (k * n) (k * m) = k * dist n m
[PROOFSTEP]
rw [mul_comm k n, mul_comm k m, dist_mul_right, mul_comm]
[GOAL]
i j : ℕ
⊢ i < j → dist i j = max i j - min i j
[PROOFSTEP]
intro h
[GOAL]
i j : ℕ
h : i < j
⊢ dist i j = max i j - min i j
[PROOFSTEP]
rw [max_eq_right_of_lt h, min_eq_left_of_lt h, dist_eq_sub_of_le (Nat.le_of_lt h)]
[GOAL]
i j : ℕ
⊢ i ≥ j → dist i j = max i j - min i j
[PROOFSTEP]
intro h
[GOAL]
i j : ℕ
h : i ≥ j
⊢ dist i j = max i j - min i j
[PROOFSTEP]
rw [max_eq_left h, min_eq_right h, dist_eq_sub_of_le_right h]
[GOAL]
i j : ℕ
⊢ dist (succ i) (succ j) = dist i j
[PROOFSTEP]
simp [dist.def, succ_sub_succ]
[GOAL]
i j : ℕ
hne : i ≠ j
h : i < j
⊢ 0 < dist i j
[PROOFSTEP]
rw [dist_eq_sub_of_le (le_of_lt h)]
[GOAL]
i j : ℕ
hne : i ≠ j
h : i < j
⊢ 0 < j - i
[PROOFSTEP]
apply tsub_pos_of_lt h
[GOAL]
i j : ℕ
hne : i ≠ j
h : i = j
⊢ 0 < dist i j
[PROOFSTEP]
contradiction
[GOAL]
i j : ℕ
hne : i ≠ j
h : i > j
⊢ 0 < dist i j
[PROOFSTEP]
rw [dist_eq_sub_of_le_right (le_of_lt h)]
[GOAL]
i j : ℕ
hne : i ≠ j
h : i > j
⊢ 0 < i - j
[PROOFSTEP]
apply tsub_pos_of_lt h
