Built with doc-gen4, running Lean4. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑Ctrl+↓to navigate, Ctrl+🖱️to focus. On Mac, use Cmdinstead of Ctrl.
/-
Copyright (c) 2014 Floris van Doorn. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Floris van Doorn, Jeremy Avigad

! This file was ported from Lean 3 source module data.nat.dist
! leanprover-community/mathlib commit d50b12ae8e2bd910d08a94823976adae9825718b
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Data.Nat.Order.Basic

/-!
#  Distance function on ℕ

This file defines a simple distance function on naturals from truncated subtraction.
-/


namespace Nat

/-- Distance (absolute value of difference) between natural numbers. -/
def 
dist: (n m : ℕ) → ?m.7 n m
dist
(n m :
ℕ: Type
ℕ
) := n - m + (m - n) #align nat.dist
Nat.dist: ℕ → ℕ → ℕ
Nat.dist
theorem
dist.def: ∀ (n m : ℕ), dist n m = n - m + (m - n)
dist.def
(n m :
ℕ: Type
ℕ
) :
dist: ℕ → ℕ → ℕ
dist
n m = n - m + (m - n) :=
rfl: ∀ {α : Sort ?u.315} {a : α}, a = a
rfl
#align nat.dist.def
Nat.dist.def: ∀ (n m : ℕ), dist n m = n - m + (m - n)
Nat.dist.def
theorem
dist_comm: ∀ (n m : ℕ), dist n m = dist m n
dist_comm
(n m :
ℕ: Type
ℕ
) :
dist: ℕ → ℕ → ℕ
dist
n m =
dist: ℕ → ℕ → ℕ
dist
m n :=

Goals accomplished! 🐙
n, m: ℕ


dist n m = dist m n

Goals accomplished! 🐙
#align nat.dist_comm
Nat.dist_comm: ∀ (n m : ℕ), dist n m = dist m n
Nat.dist_comm
@[simp] theorem
dist_self: ∀ (n : ℕ), dist n n = 0
dist_self
(n :
ℕ: Type
ℕ
) :
dist: ℕ → ℕ → ℕ
dist
n n =
0: ?m.1347
0
:=

Goals accomplished! 🐙

dist n n = 0

Goals accomplished! 🐙
#align nat.dist_self
Nat.dist_self: ∀ (n : ℕ), dist n n = 0
Nat.dist_self
theorem
eq_of_dist_eq_zero: ∀ {n m : ℕ}, dist n m = 0 → n = m
eq_of_dist_eq_zero
{n m :
ℕ: Type
ℕ
} (
h: dist n m = 0
h
:
dist: ℕ → ℕ → ℕ
dist
n m =
0: ?m.1811
0
) : n = m := have : n - m =
0: ?m.1849
0
:=
Nat.eq_zero_of_add_eq_zero_right: ∀ {n m : ℕ}, n + m = 0 → n = 0
Nat.eq_zero_of_add_eq_zero_right
h: dist n m = 0
h
have : n ≤ m :=
tsub_eq_zero_iff_le: ∀ {α : Type ?u.1923} [inst : CanonicallyOrderedAddMonoid α] [inst_1 : Sub α] [inst_2 : OrderedSub α] {a b : α}, a - b = 0 ↔ a ≤ b
tsub_eq_zero_iff_le
.
mp: ∀ {a b : Prop}, (a ↔ b) → a → b
mp
this: n - m = 0
this
have : m - n =
0: ?m.1988
0
:=
Nat.eq_zero_of_add_eq_zero_left: ∀ {n m : ℕ}, n + m = 0 → m = 0
Nat.eq_zero_of_add_eq_zero_left
h: dist n m = 0
h
have : m ≤ n :=
tsub_eq_zero_iff_le: ∀ {α : Type ?u.2033} [inst : CanonicallyOrderedAddMonoid α] [inst_1 : Sub α] [inst_2 : OrderedSub α] {a b : α}, a - b = 0 ↔ a ≤ b
tsub_eq_zero_iff_le
.
mp: ∀ {a b : Prop}, (a ↔ b) → a → b
mp
this: m - n = 0
this
le_antisymm: ∀ {α : Type ?u.2070} [inst : PartialOrder α] {a b : α}, a ≤ b → b ≤ a → a = b
le_antisymm
‹n ≤ m› ‹m ≤ n› #align nat.eq_of_dist_eq_zero
Nat.eq_of_dist_eq_zero: ∀ {n m : ℕ}, dist n m = 0 → n = m
Nat.eq_of_dist_eq_zero
theorem
dist_eq_zero: ∀ {n m : ℕ}, n = m → dist n m = 0
dist_eq_zero
{n m :
ℕ: Type
ℕ
} (
h: n = m
h
: n = m) :
dist: ℕ → ℕ → ℕ
dist
n m =
0: ?m.2236
0
:=

Goals accomplished! 🐙
n, m: ℕ

h: n = m


dist n m = 0
n, m: ℕ

h: n = m


dist n m = 0
n, m: ℕ

h: n = m


dist m m = 0
n, m: ℕ

h: n = m


dist n m = 0
n, m: ℕ

h: n = m


0 = 0

Goals accomplished! 🐙
#align nat.dist_eq_zero
Nat.dist_eq_zero: ∀ {n m : ℕ}, n = m → dist n m = 0
Nat.dist_eq_zero
theorem
dist_eq_sub_of_le: ∀ {n m : ℕ}, n ≤ m → dist n m = m - n
dist_eq_sub_of_le
{n m :
ℕ: Type
ℕ
} (
h: n ≤ m
h
: n ≤ m) :
dist: ℕ → ℕ → ℕ
dist
n m = m - n :=

Goals accomplished! 🐙
n, m: ℕ

h: n ≤ m


dist n m = m - n
n, m: ℕ

h: n ≤ m


dist n m = m - n
n, m: ℕ

h: n ≤ m


n - m + (m - n) = m - n
n, m: ℕ

h: n ≤ m


dist n m = m - n
n, m: ℕ

h: n ≤ m


0 + (m - n) = m - n
n, m: ℕ

h: n ≤ m


dist n m = m - n
n, m: ℕ

h: n ≤ m


m - n = m - n

Goals accomplished! 🐙
#align nat.dist_eq_sub_of_le
Nat.dist_eq_sub_of_le: ∀ {n m : ℕ}, n ≤ m → dist n m = m - n
Nat.dist_eq_sub_of_le
theorem
dist_eq_sub_of_le_right: ∀ {n m : ℕ}, m ≤ n → dist n m = n - m
dist_eq_sub_of_le_right
{n m :
ℕ: Type
ℕ
} (
h: m ≤ n
h
: m ≤ n) :
dist: ℕ → ℕ → ℕ
dist
n m = n - m :=

Goals accomplished! 🐙
n, m: ℕ

h: m ≤ n


dist n m = n - m
n, m: ℕ

h: m ≤ n


dist n m = n - m
n, m: ℕ

h: m ≤ n


dist m n = n - m
n, m: ℕ

h: m ≤ n


dist m n = n - m
n, m: ℕ

h: m ≤ n


dist m n = n - m
n, m: ℕ

h: m ≤ n


dist n m = n - m

Goals accomplished! 🐙
#align nat.dist_eq_sub_of_le_right
Nat.dist_eq_sub_of_le_right: ∀ {n m : ℕ}, m ≤ n → dist n m = n - m
Nat.dist_eq_sub_of_le_right
theorem
dist_tri_left: ∀ (n m : ℕ), m ≤ dist n m + n
dist_tri_left
(n m :
ℕ: Type
ℕ
) : m ≤
dist: ℕ → ℕ → ℕ
dist
n m + n :=
le_trans: ∀ {α : Type ?u.2645} [inst : Preorder α] {a b c : α}, a ≤ b → b ≤ c → a ≤ c
le_trans
le_tsub_add: ∀ {α : Type ?u.2718} [inst : Preorder α] [inst_1 : Add α] [inst_2 : Sub α] [inst_3 : OrderedSub α] {a b : α}, b ≤ b - a + a
le_tsub_add
(
add_le_add_right: ∀ {α : Type ?u.2799} [inst : Add α] [inst_1 : LE α] [i : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {b c : α}, b ≤ c → ∀ (a : α), b + a ≤ c + a
add_le_add_right
(
Nat.le_add_left: ∀ (n m : ℕ), n ≤ m + n
Nat.le_add_left
_ _)
_: ?m.2800
_
) #align nat.dist_tri_left
Nat.dist_tri_left: ∀ (n m : ℕ), m ≤ dist n m + n
Nat.dist_tri_left
theorem
dist_tri_right: ∀ (n m : ℕ), m ≤ n + dist n m
dist_tri_right
(n m :
ℕ: Type
ℕ
) : m ≤ n +
dist: ℕ → ℕ → ℕ
dist
n m :=

Goals accomplished! 🐙
n, m: ℕ


m ≤ n + dist n m
n, m: ℕ


m ≤ n + dist n m
n, m: ℕ


m ≤ dist n m + n
n, m: ℕ


m ≤ dist n m + n
n, m: ℕ


m ≤ dist n m + n
n, m: ℕ


m ≤ n + dist n m

Goals accomplished! 🐙
#align nat.dist_tri_right
Nat.dist_tri_right: ∀ (n m : ℕ), m ≤ n + dist n m
Nat.dist_tri_right
theorem
dist_tri_left': ∀ (n m : ℕ), n ≤ dist n m + m
dist_tri_left'
(n m :
ℕ: Type
ℕ
) : n ≤
dist: ℕ → ℕ → ℕ
dist
n m + m :=

Goals accomplished! 🐙
n, m: ℕ


n ≤ dist n m + m
n, m: ℕ


n ≤ dist n m + m
n, m: ℕ


n ≤ dist m n + m
n, m: ℕ


n ≤ dist m n + m
n, m: ℕ


n ≤ dist m n + m
n, m: ℕ


n ≤ dist n m + m

Goals accomplished! 🐙
#align nat.dist_tri_left'
Nat.dist_tri_left': ∀ (n m : ℕ), n ≤ dist n m + m
Nat.dist_tri_left'
theorem
dist_tri_right': ∀ (n m : ℕ), n ≤ m + dist n m
dist_tri_right'
(n m :
ℕ: Type
ℕ
) : n ≤ m +
dist: ℕ → ℕ → ℕ
dist
n m :=

Goals accomplished! 🐙
n, m: ℕ


n ≤ m + dist n m
n, m: ℕ


n ≤ m + dist n m
n, m: ℕ


n ≤ m + dist m n
n, m: ℕ


n ≤ m + dist m n
n, m: ℕ


n ≤ m + dist m n
n, m: ℕ


n ≤ m + dist n m

Goals accomplished! 🐙
#align nat.dist_tri_right'
Nat.dist_tri_right': ∀ (n m : ℕ), n ≤ m + dist n m
Nat.dist_tri_right'
theorem
dist_zero_right: ∀ (n : ℕ), dist n 0 = n
dist_zero_right
(n :
ℕ: Type
ℕ
) :
dist: ℕ → ℕ → ℕ
dist
n
0: ?m.3349
0
= n :=
Eq.trans: ∀ {α : Sort ?u.3362} {a b c : α}, a = b → b = c → a = c
Eq.trans
(
dist_eq_sub_of_le_right: ∀ {n m : ℕ}, m ≤ n → dist n m = n - m
dist_eq_sub_of_le_right
(
zero_le: ∀ (n : ℕ), 0 ≤ n
zero_le
n)) (
tsub_zero: ∀ {α : Type ?u.3374} [inst : PartialOrder α] [inst_1 : AddCommMonoid α] [inst_2 : Sub α] [inst : OrderedSub α] (a : α), a - 0 = a
tsub_zero
n) #align nat.dist_zero_right
Nat.dist_zero_right: ∀ (n : ℕ), dist n 0 = n
Nat.dist_zero_right
theorem
dist_zero_left: ∀ (n : ℕ), dist 0 n = n
dist_zero_left
(n :
ℕ: Type
ℕ
) :
dist: ℕ → ℕ → ℕ
dist
0: ?m.3457
0
n = n :=
Eq.trans: ∀ {α : Sort ?u.3470} {a b c : α}, a = b → b = c → a = c
Eq.trans
(
dist_eq_sub_of_le: ∀ {n m : ℕ}, n ≤ m → dist n m = m - n
dist_eq_sub_of_le
(
zero_le: ∀ (n : ℕ), 0 ≤ n
zero_le
n)) (
tsub_zero: ∀ {α : Type ?u.3482} [inst : PartialOrder α] [inst_1 : AddCommMonoid α] [inst_2 : Sub α] [inst : OrderedSub α] (a : α), a - 0 = a
tsub_zero
n) #align nat.dist_zero_left
Nat.dist_zero_left: ∀ (n : ℕ), dist 0 n = n
Nat.dist_zero_left
theorem
dist_add_add_right: ∀ (n k m : ℕ), dist (n + k) (m + k) = dist n m
dist_add_add_right
(n k m :
ℕ: Type
ℕ
) :
dist: ℕ → ℕ → ℕ
dist
(n + k) (m + k) =
dist: ℕ → ℕ → ℕ
dist
n m := calc
dist: ℕ → ℕ → ℕ
dist
(n + k) (m + k) = n + k - (m + k) + (m + k - (n + k)) :=
rfl: ∀ {α : Sort ?u.3875} {a : α}, a = a
rfl
_: ?m✝
_
= n - m + (m + k - (n + k)) :=

Goals accomplished! 🐙
n, k, m: ℕ


n + k - (m + k) + (m + k - (n + k)) = n - m + (m + k - (n + k))
n, k, m: ℕ


n + k - (m + k) + (m + k - (n + k)) = n - m + (m + k - (n + k))
n, k, m: ℕ


n - m + (m + k - (n + k)) = n - m + (m + k - (n + k))

Goals accomplished! 🐙
_: ?m✝
_
= n - m + (m - n) :=

Goals accomplished! 🐙
n, k, m: ℕ


n - m + (m + k - (n + k)) = n - m + (m - n)
n, k, m: ℕ


n - m + (m + k - (n + k)) = n - m + (m - n)
n, k, m: ℕ


n - m + (m - n) = n - m + (m - n)

Goals accomplished! 🐙
#align nat.dist_add_add_right
Nat.dist_add_add_right: ∀ (n k m : ℕ), dist (n + k) (m + k) = dist n m
Nat.dist_add_add_right
theorem
dist_add_add_left: ∀ (k n m : ℕ), dist (k + n) (k + m) = dist n m
dist_add_add_left
(k n m :
ℕ: Type
ℕ
) :
dist: ℕ → ℕ → ℕ
dist
(k + n) (k + m) =
dist: ℕ → ℕ → ℕ
dist
n m :=

Goals accomplished! 🐙
k, n, m: ℕ


dist (k + n) (k + m) = dist n m
k, n, m: ℕ


dist (k + n) (k + m) = dist n m
k, n, m: ℕ


dist (n + k) (k + m) = dist n m
k, n, m: ℕ


dist (k + n) (k + m) = dist n m
k, n, m: ℕ


dist (n + k) (m + k) = dist n m
k, n, m: ℕ


dist (n + k) (m + k) = dist n m
k, n, m: ℕ


dist (n + k) (m + k) = dist n m
k, n, m: ℕ


dist (k + n) (k + m) = dist n m

Goals accomplished! 🐙
#align nat.dist_add_add_left
Nat.dist_add_add_left: ∀ (k n m : ℕ), dist (k + n) (k + m) = dist n m
Nat.dist_add_add_left
theorem
dist_eq_intro: ∀ {n m k l : ℕ}, n + m = k + l → dist n k = dist l m
dist_eq_intro
{n m k l :
ℕ: Type
ℕ
} (
h: n + m = k + l
h
: n + m = k + l) :
dist: ℕ → ℕ → ℕ
dist
n k =
dist: ℕ → ℕ → ℕ
dist
l m := calc
dist: ℕ → ℕ → ℕ
dist
n k =
dist: ℕ → ℕ → ℕ
dist
(n + m) (k + m) :=

Goals accomplished! 🐙
n, m, k, l: ℕ

h: n + m = k + l


dist n k = dist (n + m) (k + m)
n, m, k, l: ℕ

h: n + m = k + l


dist n k = dist (n + m) (k + m)
n, m, k, l: ℕ

h: n + m = k + l


dist n k = dist n k

Goals accomplished! 🐙
_: ?m✝
_
=
dist: ℕ → ℕ → ℕ
dist
(k + l) (k + m) :=

Goals accomplished! 🐙
n, m, k, l: ℕ

h: n + m = k + l


dist (n + m) (k + m) = dist (k + l) (k + m)
n, m, k, l: ℕ

h: n + m = k + l


dist (n + m) (k + m) = dist (k + l) (k + m)
n, m, k, l: ℕ

h: n + m = k + l


dist (k + l) (k + m) = dist (k + l) (k + m)

Goals accomplished! 🐙
_: ?m✝
_
=
dist: ℕ → ℕ → ℕ
dist
l m :=

Goals accomplished! 🐙
n, m, k, l: ℕ

h: n + m = k + l


dist (k + l) (k + m) = dist l m
n, m, k, l: ℕ

h: n + m = k + l


dist (k + l) (k + m) = dist l m
n, m, k, l: ℕ

h: n + m = k + l


dist l m = dist l m

Goals accomplished! 🐙
#align nat.dist_eq_intro
Nat.dist_eq_intro: ∀ {n m k l : ℕ}, n + m = k + l → dist n k = dist l m
Nat.dist_eq_intro
theorem
dist.triangle_inequality: ∀ (n m k : ℕ), dist n k ≤ dist n m + dist m k
dist.triangle_inequality
(n m k :
ℕ: Type
ℕ
) :
dist: ℕ → ℕ → ℕ
dist
n k ≤
dist: ℕ → ℕ → ℕ
dist
n m +
dist: ℕ → ℕ → ℕ
dist
m k :=

Goals accomplished! 🐙
n, m, k: ℕ


dist n k ≤ dist n m + dist m k
n, m, k: ℕ


dist n k ≤ dist n m + dist m k

Goals accomplished! 🐙
n, m, k: ℕ


dist n m + dist m k = n - m + (m - k) + (k - m + (m - n))

Goals accomplished! 🐙
n, m, k: ℕ


dist n k ≤ dist n m + dist m k
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
n, m, k: ℕ

this: dist n m + dist m k = n - m + (m - k) + (k - m + (m - n))


dist n k ≤ n - m + (m - k) + (k - m + (m - n))
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
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))
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))
n, m, k: ℕ


dist n k ≤ dist n m + dist m k

Goals accomplished! 🐙
#align nat.dist.triangle_inequality
Nat.dist.triangle_inequality: ∀ (n m k : ℕ), dist n k ≤ dist n m + dist m k
Nat.dist.triangle_inequality
theorem
dist_mul_right: ∀ (n k m : ℕ), dist (n * k) (m * k) = dist n m * k
dist_mul_right
(n k m :
ℕ: Type
ℕ
) :
dist: ℕ → ℕ → ℕ
dist
(n * k) (m * k) =
dist: ℕ → ℕ → ℕ
dist
n m * k :=

Goals accomplished! 🐙
n, k, m: ℕ


dist (n * k) (m * k) = dist n m * k
n, k, m: ℕ


dist (n * k) (m * k) = dist n m * k
n, k, m: ℕ


n * k - m * k + (m * k - n * k) = dist n m * k
n, k, m: ℕ


dist (n * k) (m * k) = dist n m * k
n, k, m: ℕ


n * k - m * k + (m * k - n * k) = (n - m + (m - n)) * k
n, k, m: ℕ


dist (n * k) (m * k) = dist n m * k
n, k, m: ℕ


n * k - m * k + (m * k - n * k) = (n - m) * k + (m - n) * k
n, k, m: ℕ


dist (n * k) (m * k) = dist n m * k
n, k, m: ℕ


n * k - m * k + (m * k - n * k) = n * k - m * k + (m - n) * k
n, k, m: ℕ


dist (n * k) (m * k) = dist n m * k
n, k, m: ℕ


n * k - m * k + (m * k - n * k) = n * k - m * k + (m * k - n * k)

Goals accomplished! 🐙
#align nat.dist_mul_right
Nat.dist_mul_right: ∀ (n k m : ℕ), dist (n * k) (m * k) = dist n m * k
Nat.dist_mul_right
theorem
dist_mul_left: ∀ (k n m : ℕ), dist (k * n) (k * m) = k * dist n m
dist_mul_left
(k n m :
ℕ: Type
ℕ
) :
dist: ℕ → ℕ → ℕ
dist
(k * n) (k * m) = k *
dist: ℕ → ℕ → ℕ
dist
n m :=

Goals accomplished! 🐙
k, n, m: ℕ


dist (k * n) (k * m) = k * dist n m
k, n, m: ℕ


dist (k * n) (k * m) = k * dist n m
k, n, m: ℕ


dist (n * k) (k * m) = k * dist n m
k, n, m: ℕ


dist (k * n) (k * m) = k * dist n m
k, n, m: ℕ


dist (n * k) (m * k) = k * dist n m
k, n, m: ℕ


dist (k * n) (k * m) = k * dist n m
k, n, m: ℕ


dist n m * k = k * dist n m
k, n, m: ℕ


dist (k * n) (k * m) = k * dist n m
k, n, m: ℕ


k * dist n m = k * dist n m

Goals accomplished! 🐙
#align nat.dist_mul_left
Nat.dist_mul_left: ∀ (k n m : ℕ), dist (k * n) (k * m) = k * dist n m
Nat.dist_mul_left
theorem
dist_eq_max_sub_min: ∀ {i j : ℕ}, dist i j = max i j - min i j
dist_eq_max_sub_min
{i j :
ℕ: Type
ℕ
} :
dist: ℕ → ℕ → ℕ
dist
i j = (
max: {α : Type ?u.10129} → [self : Max α] → α → α → α
max
i j) -
min: {α : Type ?u.10144} → [self : Min α] → α → α → α
min
i j :=
Or.elim: ∀ {a b c : Prop}, a ∨ b → (a → c) → (b → c) → c
Or.elim
(
lt_or_ge: ∀ {α : Type ?u.10205} [inst : LinearOrder α] (a b : α), a < b ∨ a ≥ b
lt_or_ge
i j) (

Goals accomplished! 🐙
i, j: ℕ


i < j → dist i j = max i j - min i j
i, j: ℕ

h: i < j


dist i j = max i j - min i j
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
i, j: ℕ

h: i < j


dist i j = max i j - min i j
i, j: ℕ

h: i < j


dist i j = j - min i j
i, j: ℕ

h: i < j


dist i j = max i j - min i j
i, j: ℕ

h: i < j


dist i j = j - i
i, j: ℕ

h: i < j


dist i j = max i j - min i j
i, j: ℕ

h: i < j


j - i = j - i

Goals accomplished! 🐙
) (

Goals accomplished! 🐙
i, j: ℕ


i ≥ j → dist i j = max i j - min i j
i, j: ℕ

h: i ≥ j


dist i j = max i j - min i j
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
i, j: ℕ

h: i ≥ j


dist i j = max i j - min i j
i, j: ℕ

h: i ≥ j


dist i j = i - min i j
i, j: ℕ

h: i ≥ j


dist i j = max i j - min i j
i, j: ℕ

h: i ≥ j


dist i j = i - j
i, j: ℕ

h: i ≥ j


dist i j = max i j - min i j
i, j: ℕ

h: i ≥ j


i - j = i - j

Goals accomplished! 🐙
) theorem
dist_succ_succ: ∀ {i j : ℕ}, dist (succ i) (succ j) = dist i j
dist_succ_succ
{i j :
Nat: Type
Nat
} :
dist: ℕ → ℕ → ℕ
dist
(
succ: ℕ → ℕ
succ
i) (
succ: ℕ → ℕ
succ
j) =
dist: ℕ → ℕ → ℕ
dist
i j :=

Goals accomplished! 🐙
i, j: ℕ


dist (succ i) (succ j) = dist i j

Goals accomplished! 🐙
#align nat.dist_succ_succ
Nat.dist_succ_succ: ∀ {i j : ℕ}, dist (succ i) (succ j) = dist i j
Nat.dist_succ_succ
theorem
dist_pos_of_ne: ∀ {i j : ℕ}, i ≠ j → 0 < dist i j
dist_pos_of_ne
{i j :
Nat: Type
Nat
} : i ≠ j →
0: ?m.12049
0
<
dist: ℕ → ℕ → ℕ
dist
i j := fun
hne: ?m.12089
hne
=>
Nat.lt_by_cases: ∀ {a b : ℕ} {C : Sort ?u.12091}, (a < b → C) → (a = b → C) → (b < a → C) → C
Nat.lt_by_cases
(fun
h: i < j
h
: i < j =>

Goals accomplished! 🐙
i, j: ℕ

hne: i ≠ j

h: i < j


0 < dist i j
i, j: ℕ

hne: i ≠ j

h: i < j


0 < dist i j
i, j: ℕ

hne: i ≠ j

h: i < j


0 < j - i
i, j: ℕ

hne: i ≠ j

h: i < j


0 < j - i
i, j: ℕ

hne: i ≠ j

h: i < j


0 < j - i
i, j: ℕ

hne: i ≠ j

h: i < j


0 < dist i j

Goals accomplished! 🐙
) (fun
h: i = j
h
: i = j =>

Goals accomplished! 🐙
i, j: ℕ

hne: i ≠ j

h: i = j


0 < dist i j

Goals accomplished! 🐙
) fun
h: i > j
h
: i > j =>

Goals accomplished! 🐙
i, j: ℕ

hne: i ≠ j

h: i > j


0 < dist i j
i, j: ℕ

hne: i ≠ j

h: i > j


0 < dist i j
i, j: ℕ

hne: i ≠ j

h: i > j


0 < i - j
i, j: ℕ

hne: i ≠ j

h: i > j


0 < i - j
i, j: ℕ

hne: i ≠ j

h: i > j


0 < i - j
i, j: ℕ

hne: i ≠ j

h: i > j


0 < dist i j

Goals accomplished! 🐙
#align nat.dist_pos_of_ne
Nat.dist_pos_of_ne: ∀ {i j : ℕ}, i ≠ j → 0 < dist i j
Nat.dist_pos_of_ne
end Nat