∀ {α : Type u_1} [inst : CommMonoidWithZero α] (motive : NormalizationMonoid α → Prop) (x : NormalizationMonoid α),
  (∀ (u : α → αˣ) (normUnit_zero : u 0 = 1) (normUnit_mul : ∀ {a b : α}, a ≠ 0 → b ≠ 0 → u (a * b) = u a * u b)
      (normUnit_coe_units : ∀ (u_1 : αˣ), u ↑u_1 = u_1⁻¹),
      motive
        { normUnit := u, normUnit_zero := normUnit_zero, normUnit_mul := normUnit_mul,
          normUnit_coe_units := normUnit_coe_units }) →
    motive x