no goals
n m k l : ℕ
h : n + m = k + l
⊢ dist n k = dist (n + m) (k + m)
rw [dist_add_add_right]
no goals
n m k l : ℕ
h : n + m = k + l
⊢ dist (n + m) (k + m) = dist (k + l) (k + m)
rw [h]
no goals
n m k l : ℕ
h : n + m = k + l
⊢ dist (k + l) (k + m) = dist l m
rw [dist_add_add_left]