Reference · Natural numbers

rainbow.math.nat.semiring

Natural numberssrc/rainbow/math/nat/semiring.clj0 definitions, 6 theorems

Constructive natural semiring laws needed by rational proof data.

nat/add-left-cancel :
  (prefix left right : ℕ)
  (same : algebra/nat-add prefix left = algebra/nat-add prefix right)
  → left = right

nat/multiply-one-right :
  (value : ℕ)
  → nat/multiply value 1 = value

nat/multiply-associative :
  (left middle right : ℕ)
  → nat/multiply (nat/multiply left middle) right = nat/multiply left (nat/multiply middle right)

nat/multiply-swap-right :
  (left middle right : ℕ)
  → nat/multiply (nat/multiply left middle) right = nat/multiply (nat/multiply left right) middle

nat/multiply-four-reorder :
  (first second third fourth : ℕ)
  → nat/multiply (nat/multiply first second) (nat/multiply third fourth) = nat/multiply (nat/multiply first third) (nat/multiply second fourth)

nat/multiply-successor-right-cancel :
  (left right factor : ℕ)
  (same : nat/multiply left (data/succ factor) = nat/multiply right (data/succ factor))
  → left = right