True ↔ ∀ (f : ℝ → ℝ), (∀ (h : ℝ), 0 < h → Continuous fun x => f (x + h) - f x) → ∃ g a, Continuous g ∧ (∀ (x y : ℝ), a (x + y) = a x + a y) ∧ f = g + a