∀n:ℕ. ∀a:ℙ^n.  (r0 < ||a||)
{ (Auto THEN D -1 THEN Unhide THEN Auto) }
1. n : ℕ
2. a : ℝ^n + 1
3. ∃k:ℕn + 1. a k ≠ r0
⊢ r0 < ||a||