Reference · Natural numbers

rainbow.math.nat.add-order

Natural numberssrc/rainbow/math/nat/add_order.clj0 definitions, 2 theorems

Additive monotonicity building blocks for the convergence proof: a natural number is at most itself plus anything, and in particular at most its own double. `nat/at-most a b` unfolds to the existence of a witness `extra` with `a + extra = b`, so these follow directly by supplying the witness and reflexivity -- no induction. They feed the nnrat multiplication-monotonicity step `(1/2)*d <= d` and thence the geometric-sequence monotonicity in the convergence development. Requires `nat/at-most`, `algebra/nat-add`, and `proposition/witness`.

nat/le-add-right :
  (x y : ℕ)
  → x ≤ algebra/nat-add x y

nat/le-add-self :
  (x : ℕ)
  → x ≤ algebra/nat-add x x