The positive natural numbers #
This file develops the type ℕ+
or PNat
, the subtype of natural numbers that are positive.
It is defined in Data.PNat.Defs
, but most of the development is deferred to here so
that Data.PNat.Defs
can have very few imports.
The order isomorphism between ℕ and ℕ+ given by succ
.
Equations
Instances For
@[simp]
@[simp]
@[simp]
b is greater one if any a is less than b
Subtraction a - b is defined in the obvious way when a > b, and by a - b = 1 if a ≤ b.