properties of inequality
successor and predecessor
Many lemmas are proven more generally in mathlib
p is a (decidable) predicate on
hp : ∃ (n : ℕ), p n is a proof that
there exists some natural number satisfying
Nat.find hp is the
smallest natural number satisfying
p. Note that
Nat.find is protected,
meaning that you can't just write
find, even if the
nat namespace is open.
The API for
Nat.find_specis the proof that
Nat.find_minis the proof that if
m < Nat.find hpthen
mdoes not satisfy
Nat.find_min'is the proof that if
Nat.find hp ≤ m.
The String representation produced by toDigitsCore has the proper length relative to
the number of digits in
n < e for some base
b. Since this works with any base greater
than one, it can be used for binary, decimal, and hex.
The core implementation of
Nat.repr returns a String with length less than or equal to the
number of digits in the decimal number (represented by
e). For example, the decimal string
representation of any number less than 1000 (10 ^ 3) has a length less than or equal to 3.