about taking limitation in the proof of lean4

Stream: lean4

[Chenyi Li]

If I have a lemma claiming that for any $h>0$, we have $\frac{f(x)-f(x-h)}{h} \leq a$, and assuming that $f(x)$ is derivative within an interval around x. How to show that $f'(x) \leq a$. In the proof using natural language, we claim this is done by taking a limitation as $h \to 0$. How can I do this in lean? Thanks very much for helping.