rainbow.math.nat.distance

algebra/heterogeneous-add

DefinitionSource, line 47

algebra/heterogeneous-add.{u, v, w} :
  (A : Type u) (B : Type v) (C : Type w) (dictionary : A → B → C) (x₁ : A) (x₂ : B)
  → C

algebra/homogeneous-add-instance

DefinitionSource, line 63

algebra/homogeneous-add-instance.{u} :
  (A : Type u) (dictionary : A → A → A) (x₁ x₂ : A)
  → A

nat/distance

DefinitionSource, line 77

nat/distance :
  (x₁ x₂ : ℕ)
  → ℕ

ℕ = data/Nat

nat/distance-successor

TheoremHolds by unfolding a definitionNo axiomsSource, line 105

nat/distance-successor :
  (left right : ℕ)
  → nat/distance (data/succ left) (data/succ right) = nat/distance left right

= = equality/Eqℕ = data/Nat

nat/distance-commutative

TheoremFor all inputsNo axiomsSource, line 126

nat/distance-commutative :
  (left right : ℕ)
  → nat/distance left right = nat/distance right left

= = equality/Eqℕ = data/Nat

nat/distance-add-left

TheoremFor all inputsNo axiomsSource, line 187

nat/distance-add-left :
  (prefix left right : ℕ)
  → nat/distance (algebra/nat-add prefix left) (algebra/nat-add prefix right) = nat/distance left right

= = equality/Eqℕ = data/Nat

nat/distance-add-right

TheoremFor all inputsNo axiomsSource, line 213

nat/distance-add-right :
  (left suffix right : ℕ)
  → nat/distance (algebra/nat-add left suffix) (algebra/nat-add right suffix) = nat/distance left right

= = equality/Eqℕ = data/Nat

nat/distance-right-bound

TheoremFor all inputsNo axiomsSource, line 259

nat/distance-right-bound :
  (left right : ℕ)
  → right ≤ algebra/nat-add left (nat/distance left right)

ℕ = data/Nat≤ = nat/at-most

nat/distance-left-bound

TheoremFor all inputsNo axiomsSource, line 345

nat/distance-left-bound :
  (left right : ℕ)
  → right ≤ algebra/nat-add (nat/distance left right) left

ℕ = data/Nat≤ = nat/at-most