∀ {S : Type u_1} [inst : CommRing S] (I x : Ideal S) (motive : (I ≤ x ∧ ∃ x_1 ∈ x, x_1 ∉ I) → Prop)
  (x_1 : I ≤ x ∧ ∃ x_1 ∈ x, x_1 ∉ I),
  (∀ (I_le_J : I ≤ x) (x_2 : S) (hxJ : x_2 ∈ x) (hxI : x_2 ∉ I), motive ⋯) → motive x_1