case a
n p : ℕ
pp : Prime p
a✝ : ℕ
⊢ a✝ ∈ Nat.divisors p ↔ a✝ ∈ {1, p}
n p : ℕ
pp : Prime p
⊢ Nat.divisors p = {1, p}
ext
no goals
case a
n p : ℕ
pp : Prime p
a✝ : ℕ
⊢ a✝ ∈ Nat.divisors p ↔ a✝ ∈ {1, p}
rw [mem_divisors, dvd_prime pp, and_iff_left pp.ne_zero, Finset.mem_insert, Finset.mem_singleton]