rw [Square, Rectangle, uIcc_of_le (by simp; linarith), uIcc_of_le (by simp; linarith)]
z w : ℂ
c : ℝ
p : ℂ
cpos : c > 0
⊢ Square p c = Icc (-c + p.re) (c + p.re) ×ℂ Icc (-c + p.im) (c + p.im)
z w : ℂ
c : ℝ
p : ℂ
cpos : c > 0
⊢ Icc (-↑c - ↑c * I + p).re (↑c + ↑c * I + p).re ×ℂ Icc (-↑c - ↑c * I + p).im (↑c + ↑c * I + p).im =
    Icc (-c + p.re) (c + p.re) ×ℂ Icc (-c + p.im) (c + p.im)