Reference · Non-negative rationals

rainbow.math.rational.nnrat.positive-succ-form

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

A positive nnrat in make(succ p, q) form, so the reciprocal machinery (divide-self-positive / reciprocal-scale-cancel, which are stated for make(succ p, q)) applies to it. nat/successor-of-predecessor : 1 <= n -> succ (predecessor n) = n nnrat/make-succ-of-positive-numerator : 1 <= numerator c -> c ~ make (succ (predecessor (numerator c))) (denominator-predecessor c) The nnrat bridge is just: the cross-product of c and that make differ only by numerator c vs succ(pred(numerator c)), equal by the nat lemma. Axiom-free; additive.

Depends onmath.rational.nnrat.monus

nat/successor-of-predecessor :
  (n : ℕ)
  (h : 1 ≤ n)
  → data/succ (nat/predecessor n) = n

nnrat/make-succ-of-positive-numerator :
  (c : ℚ≥0)
  (h : 1 ≤ nnrat/numerator c)
  → c = data/pair ℕ ℕ (data/succ (nat/predecessor (nnrat/numerator c))) (nnrat/denominator-predecessor c)