Reference · Natural numbers

rainbow.math.nat.strict-below-split

Natural numberssrc/rainbow/math/nat/strict_below_split.clj0 definitions, 1 theorems

nat/strict-below-successor-split : strict-below i (succ m) -> (strict-below i m) or (i = m). strict-below i n unfolds to (exists extra, (succ i) + extra = n). Eliminate the existence; the witness equation succ(i)+extra = succ m gives i+extra = m (successor-injective). Case on extra: extra=0 gives i = m (add-commutative strips the +0); extra=succ e gives strict-below i m with witness e (add-commutative moves the successor across). The reusable decomposition needed for 'indexed-max dominates every index below n' -- a pure nat lemma, off the trusted base.

Depends onmath.nat.infinite

nat/strict-below-successor-split :
  (i m : ℕ) (h : nat/strict-below i (data/succ m))
  → proposition/disjunction (nat/strict-below i m) (i = m)