simp only [norm_eq_abs, abs_ofReal, norm_mul, abs_I, mul_one, abs_of_pos hσ.1]
N : ℕ
Npos : 1 ≤ N
σ t : ℝ
hσ : σ ∈ Ioc 0 2
ht : 2 ≤ |t|
⊢ ‖↑σ‖ + ‖↑t * I‖ ≤ 2 * |t|
N : ℕ
Npos : 1 ≤ N
σ t : ℝ
hσ : σ ∈ Ioc 0 2
ht : 2 ≤ |t|
⊢ σ + |t| ≤ 2 * |t|