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

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