BKLNW.Gp''_nonneg

lemma Gp''_nonneg {A₁ A₂ E : ℝ} (hA1 : 0 ≤ A₁) (hA2 : 0 ≤ A₂) (hE : 0 ≤ E)    {y : ℝ} (hy20 : 20 ≤ y) : 0 ≤ Gp'' A₁ A₂ E y := by  have hy3 : (0 : ℝ) ≤ y ^ 3 := pow_nonneg (by linarith) 3  unfold Gp'' expTdd  have t1 : (0 : ℝ) ≤ A₁ *      (((1 / 2 : ℝ) ^ 2 * y ^ 5 - 10 * (1 / 2) * y ^ 4 + 20 * y ^ 3) * Real.exp (-((1 / 2 : ℝ) * y))) := by    apply mul_nonneg hA1    apply mul_nonneg _ (Real.exp_pos _).le    have hbr : (0 : ℝ) ≤ (1 / 4 : ℝ) * y ^ 2 - 5 * y + 20 := by nlinarith [hy20, sq_nonneg (y - 20)]    nlinarith [mul_nonneg hy3 hbr]  have t2 : (0 : ℝ) ≤ A₂ *      (((2 / 3 : ℝ) ^ 2 * y ^ 5 - 10 * (2 / 3) * y ^ 4 + 20 * y ^ 3) * Real.exp (-((2 / 3 : ℝ) * y))) := by    apply mul_nonneg hA2    apply mul_nonneg _ (Real.exp_pos _).le    have hbr : (0 : ℝ) ≤ (4 / 9 : ℝ) * y ^ 2 - (20 / 3) * y + 20 := by nlinarith [hy20, sq_nonneg (y - 20)]    nlinarith [mul_nonneg hy3 hbr]  have t3 : (0 : ℝ) ≤ E * (20 * y ^ 3) := mul_nonneg hE (by positivity)  linarith [t1, t2, t3]