use a * c - b * d, a * d + b * c
case intro.intro.intro.intro
α : Type u_1
inst✝ : CommRing α
a b c d : α
⊢ SumOfSquares ((a ^ 2 + b ^ 2) * (c ^ 2 + d ^ 2))
case h
α : Type u_1
inst✝ : CommRing α
a b c d : α
⊢ (a ^ 2 + b ^ 2) * (c ^ 2 + d ^ 2) = (a * c - b * d) ^ 2 + (a * d + b * c) ^ 2