Identity map of Natural Numbers is strictly monotone

Stream: mathlib4

[Jihoon Hyun]

The proof is very trivial, but I wish I had one defined because it's very specific. Please tell me if this is not a good idea.

theorem nat_identity_strictMono :
  StrictMono (λ (n : ℕ) ↦ n) := by
  unfold StrictMono
  simp only [imp_self, forall_const]

[Chris Hughes]

We already have strictMono_id which says that the identity function is strictly monotonic on any preorder.

[Jihoon Hyun]

oh.