by_cases h : n < N
case intro.refine_2
n✝ : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
hu : ∀ᶠ (n : ℕ) in atTop, u (n + 1) ≤ u n
N : ℕ
hN : ∀ b ≥ N, u (b + 1) ≤ u b
v : ℕ → ℝ := fun n => u (if n < N then N else n)
n : ℕ
⊢ v (n + 1) ≤ v n
case pos
n✝ : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
hu : ∀ᶠ (n : ℕ) in atTop, u (n + 1) ≤ u n
N : ℕ
hN : ∀ b ≥ N, u (b + 1) ≤ u b
v : ℕ → ℝ := fun n => u (if n < N then N else n)
n : ℕ
h : n < N
⊢ v (n + 1) ≤ v n

case neg
n✝ : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
hu : ∀ᶠ (n : ℕ) in atTop, u (n + 1) ≤ u n
N : ℕ
hN : ∀ b ≥ N, u (b + 1) ≤ u b
v : ℕ → ℝ := fun n => u (if n < N then N else n)
n : ℕ
h : ¬n < N
⊢ v (n + 1) ≤ v n