R : Type u_1
inst✝ : LinearOrderedCommRing R
a : ℍ[R]
⊢ 0 ≤ a.re ^ 2 + a.imI ^ 2 + a.imJ ^ 2 + a.imK ^ 2
R : Type u_1
inst✝ : LinearOrderedCommRing R
a : ℍ[R]
⊢ 0 ≤ ↑normSq a
rw [normSq_def']
no goals
R : Type u_1
inst✝ : LinearOrderedCommRing R
a : ℍ[R]
⊢ 0 ≤ a.re ^ 2 + a.imI ^ 2 + a.imJ ^ 2 + a.imK ^ 2
apply_rules [sq_nonneg, add_nonneg]