Theorem: HTPI.prime_NeZero (HTPILib/Chap7.lean)

State before:
p : ℕ
h : prime p
⊢ NeZero p
Tactic:
rewrite [neZero_iff]
State after:
p : ℕ
h : prime p
⊢ p ≠ 0

State before:
p : ℕ
h : prime p
⊢ p ≠ 0
Tactic:
define at h
State after:
p : ℕ
h : 2 ≤ p ∧ ¬∃ a b, a * b = p ∧ a < p ∧ b < p
⊢ p ≠ 0

State before:
p : ℕ
h : 2 ≤ p ∧ ¬∃ a b, a * b = p ∧ a < p ∧ b < p
⊢ p ≠ 0
Tactic:
linarith
State after:
no goals