Theorem: square_neg (PrimeNumberTheoremAnd/Rectangle.lean)

State before:
z w : ℂ
c✝ : ℝ
p : ℂ
c : ℝ
⊢ Square p (-c) = Square p c
Tactic:
simpa [Square] using Rectangle.symm
State after:
no goals