The units of the natural numbers as a Monoid and AddMonoid

theorem Nat.units_eq_one (u : ℕˣ) : u = 1

theorem Nat.addUnits_eq_zero (u : AddUnits ℕ) : u = 0

@[simp]

theorem Nat.isUnit_iff {n : ℕ} : IsUnit n ↔ n = 1

instance Nat.unique_units : Unique ℕˣ

instance Nat.unique_addUnits : Unique (AddUnits ℕ)