no goals
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizationMonoid α
a : α
b : Associates α
⊢ ∀ (a_1 : α),
    a ∣ Associates.out (Quotient.mk (Associated.setoid α) a_1) ↔ Associates.mk a ≤ Quotient.mk (Associated.setoid α) a_1
simp [Associates.out_mk, Associates.quotient_mk_eq_mk, mk_le_mk_iff_dvd_iff]