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

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