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

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

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