x✝ x y : ℝ
h : x ≤ y
n : ℕ
⊢ sqrt (2 + sqrtTwoAddSeries x n) ≤ sqrt (2 + sqrtTwoAddSeries y n)
x✝ x y : ℝ
h : x ≤ y
n : ℕ
⊢ sqrtTwoAddSeries x (n + 1) ≤ sqrtTwoAddSeries y (n + 1)
rw [sqrtTwoAddSeries, sqrtTwoAddSeries]
no goals
x✝ x y : ℝ
h : x ≤ y
n : ℕ
⊢ sqrt (2 + sqrtTwoAddSeries x n) ≤ sqrt (2 + sqrtTwoAddSeries y n)
exact sqrt_le_sqrt (add_le_add_left (sqrtTwoAddSeries_monotone_left h _) _)