Theorem: DiracSeq.integrable_pnat (ForML/Dirac.lean)

State before:
n : ℕ+
⊢ 0 < ↑↑n
Tactic:
simp
State after:
no goals