refactor(analysis/asymptotics): make is_o irreducible (#2416)
`is_o` is currently not irreducible. Since it is a complicated type, Lean can have trouble checking if two types with `is_o` are defeq or not, leading to timeouts as described in https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there.20code.20for.20X.3F/topic/undergraduate.20calculus/near/193776607
This PR makes `is_o` irreducible.
