Commit 2024-05-26 18:16 f136a3c7
View on Github →feat(Mathlib/Tactic/Positivity/Basic): positivity extension for ℕ+(PNat) (#13229)
The positivity extention to prove the positivity of ℕ+(PNat):
example (n : ℕ+) : 0 < (↑n : ℕ) := by positivity