mathlib

6e003306 - feat(algebra/squarefree): relate squarefree on naturals to factorization (#13816)

feat(algebra/squarefree): relate squarefree on naturals to factorization (#13816) Also moves `nat.two_le_iff` higher up the hierarchy since it's an elementary lemma and give it a more appropriate type. The lemma `squarefree_iff_prime_sq_not_dvd` has been deleted because it's a duplicate of a lemma which is already earlier in the same file. Co-authored-by: Bhavik Mehta <bm489@cam.ac.uk>