no goals
n p : ℕ
pp : Prime p
⊢ Nat.properDivisors p = {1}
rw [← erase_insert properDivisors.not_self_mem, insert_self_properDivisors pp.ne_zero,
  pp.divisors, pair_comm, erase_insert fun con => pp.ne_one (mem_singleton.1 con)]