R : Type u_1
inst✝ : LinearOrderedCommRing R
a : ℍ[R]
⊢ a ^ 2 = -↑(↑normSq a) ↔ star a = -a
R : Type u_1
inst✝ : LinearOrderedCommRing R
a : ℍ[R]
⊢ a ^ 2 = -↑(↑normSq a) ↔ a.re = 0
simp_rw [← star_eq_neg]
case inl
R : Type u_1
inst✝ : LinearOrderedCommRing R
⊢ 0 ^ 2 = -↑(↑normSq 0) ↔ star 0 = -0

case inr
R : Type u_1
inst✝ : LinearOrderedCommRing R
a : ℍ[R]
hq0 : a ≠ 0
⊢ a ^ 2 = -↑(↑normSq a) ↔ star a = -a
R : Type u_1
inst✝ : LinearOrderedCommRing R
a : ℍ[R]
⊢ a ^ 2 = -↑(↑normSq a) ↔ star a = -a
obtain rfl | hq0 := eq_or_ne a 0
no goals
case inl
R : Type u_1
inst✝ : LinearOrderedCommRing R
⊢ 0 ^ 2 = -↑(↑normSq 0) ↔ star 0 = -0
simp
no goals
case inr
R : Type u_1
inst✝ : LinearOrderedCommRing R
a : ℍ[R]
hq0 : a ≠ 0
⊢ a ^ 2 = -↑(↑normSq a) ↔ star a = -a
rw [← star_mul_self, ← mul_neg, ← neg_sq, sq, mul_left_inj' (neg_ne_zero.mpr hq0), eq_comm]