m n : Nat
⊢ ↑n * negOfNat m = negOfNat (m * n)
m n : Nat
⊢ negOfNat m * ↑n = negOfNat (m * n)
rw [Int.mul_comm]
no goals
m n : Nat
⊢ ↑n * negOfNat m = negOfNat (m * n)
simp [ofNat_mul_negOfNat, Nat.mul_comm]