chore(analysis/asymptotics): a few more lemmas (#5482)
* golf some proofs;
* `x ^ n = o (y ^ n)` as `n → ∞` provided that `0 ≤ x < y`;
* lemmas about `is_O _ _ ⊤` etc;
* if `is_O f g cofinite`, then for some `C>0` and any `x` such that `g x ≠ 0` we have `∥f x∥≤C*∥g x∥`.
