Theorem: PrimeRange.prodNeZero (FromTheBook/Ch02/UnboundedGaps.lean)

State before:
k : ℕ
⊢ prod k ≠ 0
Tactic:
simp [prod, PrimeRange, List.mem_filter]
State after:
no goals