Reference · Non-negative rationals

rainbow.math.rational.nnrat.add-cancellation

Non-negative rationalssrc/rainbow/math/rational/nnrat/add_cancellation.clj0 definitions, 2 theorems

Real-analysis roadmap step 3: additive cancellation for the nnrat order -- nnrat/at-most-add-right-cancel : (X + k) <= (Y + k) -> X <= Y the converse of add-monotonicity, and the piece signed order transitivity needs (it cancels the shared pos(b)+neg(b) term). Strategy: drop the closure comparison to the base cross-product with step-2 nnrat/at-most-to-cross, cancel there, then lift back with nnrat/at-most-from-cross. At the base level base(X+k)(Y+k) reduces to a nat cross-product; transport the packed product-denominators succ(combine ..) to dX*dk / dY*dk via the nnrat/denominator-combine law, normalize both sides to (A + K) and (B + K) with the nat-ring tactic (K is the shared nk-term, equal on both sides as a monomial), cancel it additively (step-1a nat/at-most-add-right-cancel), then cancel the doubled positive factor dk = succ(dpre k) twice (step-1 nat/at-most-multiply-right-cancel) to reach nX*dY <= nY*dX = base X Y. Native and axiom-free; chains rainbow.math.rational.nnrat.order-equivalence (-> nat cancellation, nat-ring) on d63.

Depends onmath.rational.nnrat.order-equivalence

nnrat/base-at-most-add-right-cancel :
  (x k y : ℚ≥0) (hb : nnrat/base-at-most (x + k) (y + k))
  → nnrat/base-at-most x y

nnrat/at-most-add-right-cancel :
  (x k y : ℚ≥0)
  (h : x + k ≤ y + k)
  → x ≤ y