Reference · Signed rationals

rainbow.math.rational.signed.add-zero-reflection

Signed rationalssrc/rainbow/math/rational/signed/add_zero_reflection.clj0 definitions, 2 theorems

A zero sum of two nonnegative signed rationals has zero summands. signed/add-zero-split-nonnegative-left signed/add-zero-split-nonnegative-right For the left summand, 0<=b and additive monotonicity give a<=a+b. If a+b~0, transport that bound to a<=0; 0<=a follows from nonnegativity, and signed antisymmetry gives a~0. The right theorem commutes the sum and reuses the left theorem. Native and axiom-free.

signed/add-zero-split-nonnegative-left :
  (left right : ℚ) (left-nonnegative : signed/nonnegative left)
  (right-nonnegative : signed/nonnegative right)
  (sum-zero : left + right = 0)
  → left = 0

signed/add-zero-split-nonnegative-right :
  (left right : ℚ) (left-nonnegative : signed/nonnegative left)
  (right-nonnegative : signed/nonnegative right)
  (sum-zero : left + right = 0)
  → right = 0