Reference · Non-negative rationals

rainbow.math.rational.nnrat.monus

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

Layer 2 of the signed->nnrat magnitude foundation: truncated subtraction on Nnrat. nnrat/monus p q -- mirrors nnrat/add but with nat/monus in the numerator (same combined denominator). Its num/den reduce definitionally to the cross forms (as nnrat/add's do). The cancellation nnrat/monus-add-cancel : q <= p -> (nnrat/monus p q) + q ~ p is what lets a nonnegative signed value's magnitude round-trip through from-nnrat. Proof: to-cross gives Bb<=A (nat) with A=num p*den q, Bb=num q*den p; the numerator of (monus p q)+q collapses M*dq + Bb*dq = (M+Bb)*dq = A*dq using nat-monus-add-cancel (M+Bb=A via the at-most witness) + distributivity; the resulting cross-product equality is a pure monomial identity discharged by the nat-ring tactic. Axiom-free; additive.

Depends onmath.rational.nnrat.order-equivalencemath.nat.monus

nnrat/monus :
  (x₁ x₂ : ℚ≥0)
  → ℚ≥0

nnrat/monus-add-cancel :
  (p q : ℚ≥0)
  (h : q ≤ p)
  → nnrat/monus p q + q = p