dist_add_add_right — Mathlib

English

For all n,m,k ∈ ℕ, dist(n+k, m+k) = dist(n,m).

Русский

Для любых n,m,k ∈ ℕ верно: dist(n+k, m+k) = dist(n,m).

LaTeX

$$$$ \operatorname{dist}(n+k, m+k) = \operatorname{dist}(n,m). $$$$

Lean4

theorem dist_add_add_right (n k m : ℕ) : dist (n + k) (m + k) = dist n m :=
  calc
    dist (n + k) (m + k) = n + k - (m + k) + (m + k - (n + k)) := rfl
    _ = n - m + (m + k - (n + k)) := by rw [@add_tsub_add_eq_tsub_right]
    _ = n - m + (m - n) := by rw [@add_tsub_add_eq_tsub_right]

Похожие утверждения