Reference · Non-negative rationals

rainbow.math.rational.nnrat.complement-proper

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

Proper raw fraction for the exact complement of a positive subunit mass.

Depends onmath.rational.nnrat.ordered-distancemath.rational.nnrat.positivemath.nat.add-order

nat/distance-at-most-upper-of-at-most :
  (left right : ℕ)
  (ordered : left ≤ right)
  → nat/distance left right ≤ right

nnrat/distance-to-one-proper-of-positive-at-most-one :
  (value : ℚ≥0)
  (bounded : value ≤ 1)
  (positive : nnrat/positive value)
  → nnrat/numerator (nnrat/distance value 1) ≤ nnrat/denominator-predecessor (nnrat/distance value 1)