have conv_imples: (p l - p t) / (l - t) < (p u - p t) / (u - t) :=
  StrictConvexOn.secant_strict_mono p_conv (a := t) (x := l) (y := u)
    (Set.mem_Icc.mpr ⟨lLeT, tLeU⟩)
    (Set.left_mem_Icc.mpr lLeU)
    (Set.right_mem_Icc.mpr lLeU)
    (ne_of_lt l_bound) (Ne.symm (ne_of_lt u_bound)) lLtU
case intro
d : ℕ
l u t : ℝ
p : ℝ → ℝ := taylorWithinEval Real.exp d (Set.Ioo l u) 0
secant : ℝ := (p l - p u) / (l - u) * (t - l) + p l
p_conv : StrictConvexOn ℝ (Set.Icc l u) p
t_neg : t < 0
l_bound : t > l
u_bound : t < u
lLeT : l ≤ t
tLeU : t ≤ u
lLeU : l ≤ u
lLtU : l < u
⊢ t.exp ≤ secant
case intro
d : ℕ
l u t : ℝ
p : ℝ → ℝ := taylorWithinEval Real.exp d (Set.Ioo l u) 0
secant : ℝ := (p l - p u) / (l - u) * (t - l) + p l
p_conv : StrictConvexOn ℝ (Set.Icc l u) p
t_neg : t < 0
l_bound : t > l
u_bound : t < u
lLeT : l ≤ t
tLeU : t ≤ u
lLeU : l ≤ u
lLtU : l < u
conv_imples : (p l - p t) / (l - t) < (p u - p t) / (u - t)
⊢ t.exp ≤ secant