Reference · Non-negative rationals

rainbow.math.rational.nnrat.unit-fraction

Non-negative rationalssrc/rainbow/math/rational/nnrat/unit_fraction.clj0 definitions, 4 theorems

Explicit positive unit fractions and their proper complements. Kernel-checked and axiom-free on D63. All identities use rational equivalence, not structural equality of raw representatives.

Depends onmath.rational.nnrat.positive

nnrat/unit-fraction-at-most-positive :
  (value : ℚ≥0) (positive : nnrat/positive value)
  → nnrat/make 1 (nnrat/denominator-predecessor value) ≤ value

nnrat/unit-fraction-positive :
  (dp : ℕ)
  → nnrat/positive (nnrat/make 1 dp)

nnrat/unit-fraction-plus-complement :
  (dp : ℕ)
  → nnrat/make dp dp + nnrat/make 1 dp = 1

nnrat/unit-fraction-complement-proper :
  (dp : ℕ)
  → nnrat/numerator (nnrat/make dp dp) ≤ nnrat/denominator-predecessor (nnrat/make dp dp)