Reference · Natural numbers

rainbow.math.nat.at-most-cancellation

Natural numberssrc/rainbow/math/nat/at_most_cancellation.clj0 definitions, 4 theorems

Real-analysis bedrock (roadmap step 1): cancellation for the nat order. ADDITIVE (step-1a): nat/at-most a b unfolds to (exists extra, a + extra = b), so cancellation is a witness manipulation -- extract the witness, reorder with the nat-ring tactic, cancel the common summand via nat/add-left-cancel: nat/at-most-add-right-cancel : (a + k) <= (b + k) -> a <= b nat/at-most-add-left-cancel : (k + a) <= (k + b) -> a <= b MULTIPLICATIVE (step-1, the base-at-most-transitivity brick): cancel a POSITIVE right factor from an order comparison: nat/at-most-multiply-right-cancel : a*(succ f) <= b*(succ f) -> a <= b proved by case-splitting decide(a<=b) with the Bool.rec equality-motive -- true branch is decide-at-most-true-sound; false branch takes b<=a (decide-at-most-false-reverse), lifts to b*k <= a*k (multiply-right-monotone), derives a*k = b*k with the hypothesis (at-most-antisymmetric), cancels the positive factor to a = b (multiply-successor-right-cancel), and rewrites to a <= b. Native and axiom-free; chains rainbow.math.nat.ring on d63.

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

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

nat/sum-zero-left :
  (x y : ℕ)
  (h : algebra/nat-add x y = 0)
  → x = 0

nat/at-most-multiply-right-cancel :
  (a b f : ℕ)
  (h : nat/multiply a (data/succ f) ≤ nat/multiply b (data/succ f))
  → a ≤ b