feat(data/pnat/basic): 0 < n as a fact (#11729)

Author: ericrbg

src/data/pnat/basic.lean

@@ -84,6 +84,9 @@ subtype.linear_order _
 
 @[simp] theorem pos (n : ℕ+) : 0 < (n : ℕ) := n.2
 
+-- see note [fact non_instances]
+lemma fact_pos (n : ℕ+) : fact (0 < ↑n) := ⟨n.pos⟩
+
 theorem eq {m n : ℕ+} : (m : ℕ) = n → m = n := subtype.eq
 
 @[simp] lemma coe_inj {m n : ℕ+} : (m : ℕ) = n ↔ m = n := set_coe.ext_iff