Theorem: LoVe.neg_Nat_mul_neg (LoVe/Lectures/LoVe13_BasicMathematicalStructures_Demo.lean)

State before:
n : ℕ
z : ℤ
⊢ -↑n * -z = ↑n * z
Tactic:
simp
State after:
no goals