no goals
S : Type ?u.795476
T : Type ?u.795479
R : Type u_1
inst✝ : CommRing R
r x y z : R
a b c : ℍ[R]
⊢ ↑(↑normSq (a + b)) = ↑(↑normSq a) + a * star b + b * star a + ↑(↑normSq b)
simp only [star_add, ← self_mul_star, mul_add, add_mul, add_assoc, add_left_comm]