Reference · Non-negative rationals

rainbow.math.rational.nnrat.additive-reassociation

Non-negative rationalssrc/rainbow/math/rational/nnrat/additive_reassociation.clj0 definitions, 3 theorems

Associativity and reusable summand reorder laws for native nonnegative rationals. The foundational associativity proof unfolds rational addition to its numerator/positive-denominator cross product and asks the verified nat semiring normalizer for a kernel-checkable equality proof. The two downstream laws are then assembled from associativity, commutativity, congruence, symmetry, and transitivity at the nnrat equivalence layer.

nnrat/add-associative :
  (a b c : ℚ≥0)
  → a + b + c = a + (b + c)

nnrat/add-swap-right :
  (a b c : ℚ≥0)
  → a + (b + c) = b + (a + c)

nnrat/add-four-reorder :
  (a b c d : ℚ≥0)
  → a + b + (c + d) = a + c + (b + d)