∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : NormalizationMonoid α] [inst_2 : UniqueFactorizationMonoid α]
  (x : α), x ≠ 0 → (0 < UniqueFactorizationMonoid.normalizedFactors x ↔ ¬IsUnit x)