∀ {G : Type u_5} {G' : Type u_8} [inst : Norm G] [inst_1 : SeminormedAddCommGroup G'] {α : Type u_17}
  [inst_2 : SemilatticeSup α] [Nonempty α] {f : α → G} {g : α → G'},
  f =O[Filter.atTop] g ↔ ∀ᶠ (n₀ : α) in Filter.atTop, ∃ c > 0, ∀ n ≥ n₀, c * ‖f n‖ ≤ ‖g n‖