D-Thomine

Sorry to bother you again, but I'm currently working on proving these lemmas ; I should have a more general version of `limsup_mul_le` with a much shorter proof (and many...

A more general version of `limsup_mul_le` is in [#18365](https://github.com/leanprover-community/mathlib4/pull/18365) (arbitrary filters, and the nonnegativity/boundedness conditions are replaced by appropriate eventual/frequent properties). Your own version should follow quite quickly from it.