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

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