feat(PNat/Basic): add three lemmas (#12479)

Three small lemmata in support of further PNat proofs

Author: rwst

Mathlib/Data/PNat/Basic.lean

@@ -314,6 +314,13 @@ theorem pow_coe (m : ℕ+) (n : ℕ) : ↑(m ^ n) = (m : ℕ) ^ n :=
   rfl
 #align pnat.pow_coe PNat.pow_coe
 
+/-- b is greater one if any a is less than b -/
+theorem one_lt_of_lt {a b : ℕ+} (hab : a < b) : 1 < b := bot_le.trans_lt hab
+
+theorem add_one (a : ℕ+) : a + 1 = succPNat a := rfl
+
+theorem lt_succ_self (a : ℕ+) : a < succPNat a := lt.base a
+
 /-- Subtraction a - b is defined in the obvious way when
   a > b, and by a - b = 1 if a ≤ b.
 -/