∀ {A : Type u_1} [inst : NormedRing A] [inst_1 : NormedAlgebra ℝ A] [inst_2 : PartialOrder A] {s : Set NNReal} (a : A)
  (motive : a ∈ {a | 0 ≤ a ∧ spectrum NNReal a ⊆ s} → Prop) (x : a ∈ {a | 0 ≤ a ∧ spectrum NNReal a ⊆ s}),
  (∀ (left : 0 ≤ a) (ha' : spectrum NNReal a ⊆ s), motive ⋯) → motive x