∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : NormalizationMonoid α] [inst_2 : UniqueFactorizationMonoid α]
  {p x : α}, x ≠ 0 → (p ∈ UniqueFactorizationMonoid.normalizedFactors x ↔ Irreducible p ∧ normalize p = p ∧ p ∣ x)