Reference · Natural numbers

rainbow.math.nat.metric

Natural numberssrc/rainbow/math/nat/metric.clj0 definitions, 3 theorems

Constructive order laws for computational natural distance.

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

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

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