R : Type u_1
inst✝¹ : CommMonoid R
inst✝ : DecidableRel Dvd.dvd
r a : R
⊢ a * a ∣ r → IsUnit a ↔ multiplicity a r ≤ 1 ∨ IsUnit a
R : Type u_1
inst✝¹ : CommMonoid R
inst✝ : DecidableRel Dvd.dvd
r : R
⊢ Squarefree r ↔ ∀ (x : R), multiplicity x r ≤ 1 ∨ IsUnit x
refine' forall_congr' fun a => _
R : Type u_1
inst✝¹ : CommMonoid R
inst✝ : DecidableRel Dvd.dvd
r a : R
⊢ ↑2 ≤ multiplicity a r ↔ 1 < multiplicity a r
R : Type u_1
inst✝¹ : CommMonoid R
inst✝ : DecidableRel Dvd.dvd
r a : R
⊢ a * a ∣ r → IsUnit a ↔ multiplicity a r ≤ 1 ∨ IsUnit a
rw [← sq, pow_dvd_iff_le_multiplicity, or_iff_not_imp_left, not_le, imp_congr _ Iff.rfl]
R : Type u_1
inst✝¹ : CommMonoid R
inst✝ : DecidableRel Dvd.dvd
r a : R
⊢ ↑(1 + 1) ≤ multiplicity a r ↔ 1 < multiplicity a r
R : Type u_1
inst✝¹ : CommMonoid R
inst✝ : DecidableRel Dvd.dvd
r a : R
⊢ ↑2 ≤ multiplicity a r ↔ 1 < multiplicity a r
rw [←one_add_one_eq_two]
no goals
R : Type u_1
inst✝¹ : CommMonoid R
inst✝ : DecidableRel Dvd.dvd
r a : R
⊢ ↑(1 + 1) ≤ multiplicity a r ↔ 1 < multiplicity a r
simpa using PartENat.add_one_le_iff_lt (PartENat.natCast_ne_top 1)