Sign of a quadratic polynomial

Stream: Is there code for X?

[Vincent Beffara]

Do we have in Mathlib that a real quadratic polynomial with negative discriminant and positive coefficient of degree zero (or two) is positive everywhere?

[Vincent Beffara]

example (a b c x : ℝ) (ha : 0 < a) (hΔ : discrim a b c < 0) : 0 < a * x * x + b * x + c := by
  have l1 : a * x * x + b * x + c = a * (x + b / (2 * a)) ^ 2 - discrim a b c / (4 * a) := by
    field_simp [discrim] ; ring
  have l2 : 0 < - discrim a b c := by linarith
  rw [l1, sub_eq_add_neg, ← neg_div] ; positivity