Reference · Non-negative rationals

rainbow.math.rational.nnrat.positive-monotone

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

B6c of the limit-reciprocal arc: positivity of an nnrat is preserved upward under <=. nat/positive-of-multiply-left : strict-below 0 (a*b) -> strict-below 0 a nnrat/positive-of-at-most : positive p -> p <= q -> positive q Since nnrat/positive p reduces to strict-below 0 (numerator p) (== 1 <= num p), and strict-below 0 X == nat/at-most (succ 0) X, this is exactly the `1 <= num(mag(x*x))` hypothesis shape used across the arc. Proof of B6c: cross-multiply (at-most-to-cross), num p * den q is positive (multiply-right-strict-monotone-positive with left=0, using denominator-positive), chain <= to num q * den p (at-most-transitive), then factor-positive drops the den p factor. factor-positive itself is a Nat.rec on a: base a=0 is the identity (both sides are strict-below 0 0), step a=succ e gives the witness directly. Axiom-free; additive; does not touch the LP checker.

Depends onmath.rational.nnrat.order-equivalencemath.rational.nnrat.positive

nat/positive-of-multiply-left :
  (a b : ℕ) (h : nat/strict-below 0 (nat/multiply a b))
  → nat/strict-below 0 a

nnrat/positive-of-at-most :
  (p q : ℚ≥0) (hp : nnrat/positive p)
  (hpq : p ≤ q)
  → nnrat/positive q