Reference · Natural numbers

rainbow.math.nat.monus

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

Truncated subtraction on Nat (monus), the missing arithmetic primitive under the signed->nnrat magnitude foundation. nat/monus 0 b = 0 nat/monus (succ a) 0 = succ a nat/monus (succ a)(succ b) = nat/monus a b (double recursion, like decide-at-most) Plus the cancellation law needed to extract a magnitude: nat/monus-add-cancel-left : nat/monus (b + d) b = d (every step is the double-recursion's definitional succ/succ collapse plus the IH, since algebra/nat-add recurses on its LEFT argument). Axiom-free; additive.

nat/monus :
  (x₁ x₂ : ℕ)
  → ℕ

nat/monus-zero-right :
  (a : ℕ)
  → nat/monus a 0 = a

nat/monus-add-cancel-left :
  (b d : ℕ)
  → nat/monus (algebra/nat-add b d) b = d