exact norm_nonneg (cons a b)
case hr
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
n : ℕ
E : Fin n → Type u_2
inst✝⁶ : (i : Fin n) → NormedAddCommGroup (E i)
inst✝⁵ : (i : Fin n) → NormedSpace 𝕜 (E i)
E₁ : Fin n → Type u_3
inst✝⁴ : (i : Fin n) → NormedAddCommGroup (E₁ i)
inst✝³ : (i : Fin n) → NormedSpace 𝕜 (E₁ i)
G : Type u_4
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
α : Fin (Nat.succ n) → Type u_5
inst✝ : (i : Fin (Nat.succ n)) → SeminormedAddGroup (α i)
a : α 0
b : (i : Fin n) → α (succ i)
⊢ 0 ≤ ‖cons a b‖
no goals