Theorem: SelbergSieve.selbergBoundingSum_ne_zero (PrimeNumberTheoremAnd/Mathlib/NumberTheory/Sieve/Selberg.lean)

State before:
s : SelbergSieve
⊢ S ≠ 0
Tactic:
apply _root_.ne_of_gt
State after:
case h
s : SelbergSieve
⊢ 0 < S

State before:
case h
s : SelbergSieve
⊢ 0 < S
Tactic:
exact s.selbergBoundingSum_pos
State after:
no goals