mathlib

0fac0807 - refactor(analysis/calculus/mean_value): Remove useless hypotheses (#10129)

refactor(analysis/calculus/mean_value): Remove useless hypotheses (#10129) Because the junk value of `deriv` is `0`, assuming `∀ x, 0 < deriv f x` implies that `f` is derivable. We thus remove all those redundant derivability assumptions.