rcases sosx with ⟨a, b, xeq⟩
α : Type u_1
inst✝ : CommRing α
x y : α
sosx : SumOfSquares x
sosy : SumOfSquares y
⊢ SumOfSquares (x * y)
case intro.intro
α : Type u_1
inst✝ : CommRing α
x y : α
sosy : SumOfSquares y
a b : α
xeq : x = a ^ 2 + b ^ 2
⊢ SumOfSquares (x * y)