English
The order on ℕ⁺ induced from ℕ agrees: (⟨n, hn⟩ ≤ ⟨k, hk⟩) iff n ≤ k.
Русский
Порядок на ℕ⁺, порождённый на ℕ, совпадает: (⟨n, hn⟩ ≤ ⟨k, hk⟩) тогда и только тогда, когда n ≤ k.
LaTeX
$$$ (n k : \\mathbb{N}) (hn : 0 < n) (hk : 0 < k),\\; \\left(\\langle n, hn \\rangle \\le \\langle k, hk \\rangle \\right) \\iff n \\le k.$$$
Lean4
/-- We now define a long list of structures on ℕ+ induced by
similar structures on ℕ. Most of these behave in a completely
obvious way, but there are a few things to be said about
subtraction, division and powers.
-/
theorem mk_le_mk (n k : ℕ) (hn : 0 < n) (hk : 0 < k) : (⟨n, hn⟩ : ℕ+) ≤ ⟨k, hk⟩ ↔ n ≤ k := by simp
