positivity
M : ℝ
h :
  ∀ (a b c : ℝ),
    |a * b * (a ^ 2 - b ^ 2) + b * c * (b ^ 2 - c ^ 2) + c * a * (c ^ 2 - a ^ 2)| ≤ M * (a ^ 2 + b ^ 2 + c ^ 2) ^ 2
α : ℝ := √2
hα : α ^ 2 = 2
a : ℝ := 2 - 3 * α
c : ℝ := 2 + 3 * α
⊢ 0 ≤ 18 ^ 2 * α ^ 2 * α
no goals