Reference · Signed rationals

rainbow.math.rational.signed.order-cancellation

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

Additive cancellation for signed-rational order. a + c <= b + c ==> a <= b c + a <= c + b ==> a <= b These are the converses of `signed/add-right-monotone` / `-left-monotone`, and the missing half of the additive order toolkit: monotonicity lets a shared summand be introduced, cancellation lets it be removed. Removing a shared summand is what turns an inequality between Lagrangian values into an inequality between the penalty terms, so this is the lemma that unlocks complementary-slackness style arguments over signed rationals. Signed order `u <= v` unfolds to the nnrat order positive u + negative v <= positive v + negative u, so both statements reduce to isolating the shared `positive c + negative c` summand and discharging it with `nnrat/at-most-add-right-cancel`. The two isolations are pure semiring reorderings, so each is a single `rainbow.math.rational.nnrat.ring` call. Native and axiom-free; chains the D63 signed order transitivity toolkit and the nnrat-ring tactic.

Depends onmath.rational.signed.order-transitivitymath.rational.nnrat.ring

signed/at-most-add-right-cancel :
  (a b c : ℚ)
  (ordered : a + c ≤ b + c)
  → a ≤ b

signed/at-most-add-left-cancel :
  (a b c : ℚ)
  (ordered : c + a ≤ c + b)
  → a ≤ b