Lemmas about Multiplicative ℕ

theorem Nat.toAdd_pow (a : Multiplicative ℕ) (b : ℕ) : Multiplicative.toAdd (a ^ b) = Multiplicative.toAdd a * b

@[simp]

theorem Nat.ofAdd_mul (a b : ℕ) : Multiplicative.ofAdd (a * b) = Multiplicative.ofAdd a ^ b