mathlib

c158ce85 - feat(analysis/calculus): converse mean value inequality (#4173)

feat(analysis/calculus): converse mean value inequality (#4173) Also restate mean value inequality in terms of `lipschitz_on_with`. From the sphere eversion project. Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>