⊢ List.Nodup (factors 2)


⊢ 2 ≠ 0
⊢ Squarefree 2
rw [squarefree_iff_nodup_factors]
⊢ List.Nodup [2]
⊢ List.Nodup (factors 2)
rw [Nat.factors_prime prime_two]
no goals
⊢ List.Nodup [2]
exact List.nodup_singleton 2
no goals
⊢ 2 ≠ 0
norm_num