Reference · Natural numbers

rainbow.math.nat.at-most-add

Natural numberssrc/rainbow/math/nat/at_most_add.clj0 definitions, 5 theorems

Three one-line order facts about addition that the program-family index arithmetic keeps needing (nat/at-most a b unfolds to exists e, a + e = b; addition recurses on its LEFT argument, so `a <= a + b` is a direct witness but `a <= b + a` needs commutativity and the nested form needs associativity): nat/at-most-add-right : a <= a + b nat/at-most-add-left : a <= b + a nat/at-most-add-nested : a + b <= a + (b + c) nat/add-left-swap : x + (d + y) = d + (x + y) (assoc, comm, assoc) nat/at-most-add-left-swap : x + (d + y) <= d + (x + y) (the same, as an order fact) The swap pair is what lets a depth d threaded on the LEFT of every family index commute past a fixed layout offset when bounding reads under extra bindings.

nat/at-most-add-right :
  (a b : ℕ)
  → a ≤ algebra/nat-add a b

nat/at-most-add-left :
  (a b : ℕ)
  → a ≤ algebra/nat-add b a

nat/at-most-add-nested :
  (a b c : ℕ)
  → algebra/nat-add a b ≤ algebra/nat-add a (algebra/nat-add b c)

nat/add-left-swap :
  (x d y : ℕ)
  → algebra/nat-add x (algebra/nat-add d y) = algebra/nat-add d (algebra/nat-add x y)

nat/at-most-add-left-swap :
  (x d y : ℕ)
  → algebra/nat-add x (algebra/nat-add d y) ≤ algebra/nat-add d (algebra/nat-add x y)