feat(Data/PNat/Basic): add order-related instances to PNat (#26453)

Add `SuccAddOrder ℕ+` and `NoMaxOrder ℕ+` instances.

Co-authored-by: jburroni <jburroni@users.noreply.github.com>

Author: jburroni

Mathlib.lean

@@ -3656,6 +3656,7 @@ import Mathlib.Data.PNat.Factors
 import Mathlib.Data.PNat.Find
 import Mathlib.Data.PNat.Interval
 import Mathlib.Data.PNat.Notation
+import Mathlib.Data.PNat.Order
 import Mathlib.Data.PNat.Prime
 import Mathlib.Data.PNat.Xgcd
 import Mathlib.Data.PSigma.Order

Mathlib/Data/PNat/Order.lean

@@ -0,0 +1,28 @@
+/-
+Copyright (c) 2025 Javier Burroni. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Javier Burroni
+-/
+import Mathlib.Algebra.Order.SuccPred
+import Mathlib.Data.PNat.Basic
+
+/-!
+# Order related instances for `ℕ+`
+-/
+
+namespace PNat
+open Nat
+
+instance instSuccOrder : SuccOrder ℕ+ :=
+  .ofSuccLeIff (· + 1) Iff.rfl
+
+instance instSuccAddOrder : SuccAddOrder ℕ+ where
+  succ_eq_add_one _ := rfl
+
+instance instNoMaxOrder : NoMaxOrder ℕ+ where
+  exists_gt n := ⟨n + 1, lt_succ_self n⟩
+
+@[simp]
+lemma succ_eq_add_one (n : ℕ+) : Order.succ n = n + 1 := rfl
+
+end PNat