no goals
K : Type u_1
E : Type ?u.5157046
inst✝ : IsROrC K
z w : K
⊢ ↑normSq (z - w) = ↑normSq z + ↑normSq w - 2 * ↑re (z * ↑(starRingEnd K) w)
simp only [normSq_add, sub_eq_add_neg, map_neg, mul_neg, normSq_neg, map_neg]