∀ {M : Type u_1} [inst : CommMonoidWithZero M] [inst_1 : NormalizationMonoid M] [inst_2 : UniqueFactorizationMonoid M]
  {a b : M}, Irreducible a → b ≠ 0 → (a ∣ UniqueFactorizationMonoid.radical b) = (a ∣ b)