no goals
α : Type ?u.249636
β : Type ?u.249639
γ : Type ?u.249642
δ : Type ?u.249645
inst✝³ : Monoid α
inst✝² : Unique αˣ
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : Unique Mˣ
p q : M
pp : Prime p
qp : Prime q
⊢ p ∣ q ↔ p = q
rw [pp.dvd_prime_iff_associated qp, ← associated_eq_eq]