Reference · Natural numbers

rainbow.math.nat.strict-below-more

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

Small reusable nat lemmas for indexed-fold attainment (pure nat, off the trusted base): nat/add-successor-right : i + succ e = succ (i + e) (add recurses left, so this needs proof) nat/strict-below-self : m < succ m nat/strict-below-weaken : i < m -> i < succ m

Depends onmath.nat.strict-below-split

nat/add-successor-right :
  (i e : ℕ)
  → algebra/nat-add i (data/succ e) = data/succ (algebra/nat-add i e)

nat/strict-below-self :
  (m : ℕ)
  → nat/strict-below m (data/succ m)

nat/strict-below-weaken :
  (i m : ℕ) (h : nat/strict-below i m)
  → nat/strict-below i (data/succ m)