lean_workbook_plus_42258

import Mathlib.Analysis.Complex.Basic

theorem lean_workbook_plus_42258 (a : ℝ) (x : ℕ → ℝ) (hx: x 0 = a) (hn: ∀ n:ℕ, x (n+1) = 2 * x n - a) : ∀ n:ℕ, x n ∈ Set.Ioo a (2 * a)   :=  by sorry