Deprecating `Order.Nat`

Stream: mathlib4

[Jeremy Tan]

I repurposed #16408 to deprecate Order.Nat. @Yaël Dillies was against this PR.

But I don't agree, and I still want this PR to go through.

[Andrew Yang]

I personally don't think OrderBot ℕ and NoMaxOrder ℕ should live in Mathlib/Order/BoundedOrder/Basic.lean and it should be in a separate file.

[Jireh Loreaux]

I agree with Yaël here.

[Yury G. Kudryashov]

On github, I've said that I have no opinion here. After reading more, I agree with Yael. Nat.find finds the least element of a nonempty set, so it make sense that this fact lives in Order.Nat.

[Yury G. Kudryashov]

If no maintainer voices support for this change in 72h, then I'm going to close this PR.