no goals
R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : WfDvdMonoid R
r : R
hr : r ≠ 0
⊢ Squarefree r ↔ ∀ (x : R), Irreducible x → ¬x * x ∣ r
simpa [hr] using (irreducible_sq_not_dvd_iff_eq_zero_and_no_irreducibles_or_squarefree r).symm