mathlib

475f18b6 - refactor(analysis/asymptotics): make `is_o`/`is_O` work with `calc` (#14129)

refactor(analysis/asymptotics): make `is_o`/`is_O` work with `calc` (#14129) Reorder arguments of `is_O_with`/`is_O`/`is_o` as well as `trans` lemmas so that they work with `calc`. Also adds `f =O[l] g` notation. Fixes #2273