mathlib

8bf24777 - feat(analysis/asymptotics): prove that a function has derivative 0 using asymptotics (#16934)

feat(analysis/asymptotics): prove that a function has derivative 0 using asymptotics (#16934) * From the sphere eversion project * Needed for computing derivatives of the parametric interval integral Co-authored by: Patrick Massot [patrickmassot@free.fr](patrickmassot@free.fr)