∀ {u v : ℕ → EReal},
  LinearGrowth.linearGrowthSup u ≠ ⊥ ∨ LinearGrowth.linearGrowthSup v ≠ ⊤ →
    LinearGrowth.linearGrowthSup u ≠ ⊤ ∨ LinearGrowth.linearGrowthSup v ≠ ⊥ →
      LinearGrowth.linearGrowthSup (u + v) ≤ LinearGrowth.linearGrowthSup u + LinearGrowth.linearGrowthSup v