Differentiable from deriv ≠ 0

Stream: Is there code for X?

[Yaël Dillies]

I just PRed docs#strict_convex_on_univ_of_deriv2_pos and it strikes me now that hf'' : differentiable ℝ (deriv f) is unneeded because of the junk value value of the derivative being 0. What's the quickest way to get differentiable ℝ (deriv f) from ∀ x, (deriv^[2] f x) < 0?

[Yury G. Kudryashov]

You can add (untested)

lemma differentiable_at_of_deriv_ne_zero (h : deriv f x ≠ 0) : differentiable_at 𝕜 f x :=
not_imp_comm.1 deriv_zero_of_not_differentiable_at h