R : Type u_1
inst✝¹ : MonoidWithZero R
inst✝ : Nontrivial R
hm : Squarefree 0
⊢ False
R : Type u_1
inst✝¹ : MonoidWithZero R
inst✝ : Nontrivial R
m : R
hm : Squarefree m
⊢ m ≠ 0
rintro rfl
no goals
R : Type u_1
inst✝¹ : MonoidWithZero R
inst✝ : Nontrivial R
hm : Squarefree 0
⊢ False
exact not_squarefree_zero hm