refine le_trans (by apply norm_add_le) ?_
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 * I‖ ≤ 2 * |t|