Cast of natural numbers: lemmas about Commute

theorem Nat.cast_commute {α : Type u_1} [NonAssocSemiring α] (n : ℕ) (x : α) : Commute (↑n) x

theorem Commute.ofNat_left {α : Type u_1} [NonAssocSemiring α] (n : ℕ) [Nat.AtLeastTwo n] (x : α) : Commute (OfNat.ofNat n) x

theorem Nat.cast_comm {α : Type u_1} [NonAssocSemiring α] (n : ℕ) (x : α) : ↑n * x = x * ↑n

theorem Nat.commute_cast {α : Type u_1} [NonAssocSemiring α] (x : α) (n : ℕ) : Commute x ↑n

theorem Commute.ofNat_right {α : Type u_1} [NonAssocSemiring α] (x : α) (n : ℕ) [Nat.AtLeastTwo n] : Commute x (OfNat.ofNat n)