Reference · Natural numbers

rainbow.math.nat.multiply-positive

Natural numberssrc/rainbow/math/nat/multiply_positive.clj0 definitions, 1 theorems

Constructive nat positivity of a product: 0 < a -> 0 < b -> 0 < a*b (strict-below form). Bottom brick of the magnitude route to signed no-zero-divisors. strict-below 0 X unfolds to exists extra, succ(0)+extra = X; the proof CPS-eliminates the two witnesses, transports a*b along a=succ(0)+ea and the inner b=succ(0)+eb (equality/substitution), landing on succ(eb + ea*b), which is positive by a direct witness.

Depends onmath.nat.infinitemath.nat.semiring

nat/multiply-positive :
  (a b : ℕ) (ha : nat/strict-below 0 a) (hb : nat/strict-below 0 b)
  → nat/strict-below 0 (nat/multiply a b)