How does nlinarith prove this conclusion?

Stream: new members

[Zhu]

I saw a proof here that used nlinarith. I tried but failed to decompose the expression with the two terms inside.
I wonder how nlinarith solves it. :thinking:

import Mathlib

example (x : ℝ) : x ^ 4 + 4 * x + 3 ≥ 0 := by
  nlinarith [sq_nonneg (x ^ 2), sq_nonneg (x + 1)]

[Kevin Buzzard]

It's $(x^2-1)^2+2(x+1)^2$ if this helps

[Derek Rhodes]

here's is one way with a calc block

import Mathlib

example (x : ℝ) : x ^ 4 + 4 * x + 3 ≥ 0 := by
  norm_num

  calc 0
    _ ≤ (x + 1) ^ 2 * ((x - 1) ^ 2) := by positivity
    _ = (x + 1) ^ 2 * (x ^ 2 - 2 * x + 1) := by ring
    --                                 |             1 is less than 3.
    _ ≤ (x + 1) ^ 2 * (x ^ 2 - 2 * x + 3) := by
      have : (1:ℝ) ≤ 3 := by norm_num
      rel [this]
    _ = x ^ 2 * x ^ 2 + 4 * x + 3 := by ring
    _ = x ^ 4 + 4 * x + 3 := by ring

[Zhu]

Thanks!

[Zhu]

It can be seen that nlinarith is quite powerful. However, it's strange that removing one of the sq_nonneg makes nlinarith unable to solve it.