have hz : (x + y) ^ 2 = z ^ 2 := by linear_combination (x + y - z) * hxyz
x y z s : ℝ
hxy : 0 ≤ x * y
hxyz : x + y + z = 0
⊢ 32 * |x * y * z * s| ≤ √2 * (x ^ 2 + y ^ 2 + z ^ 2 + s ^ 2) ^ 2
x y z s : ℝ
hxy : 0 ≤ x * y
hxyz : x + y + z = 0
hz : (x + y) ^ 2 = z ^ 2
⊢ 32 * |x * y * z * s| ≤ √2 * (x ^ 2 + y ^ 2 + z ^ 2 + s ^ 2) ^ 2