Definition 1.8.1.22.2.  Let n ∈ ℕ. We define:
ℕ≤n := {m ∈ ℕ : m ≤ n} = ℕ<(n+1)
Equality.  No proof.