∀ {S : Type u_1} [inst : CommRing S] [inst_1 : Nontrivial S] [inst_2 : IsDedekindDomain S] [inst_3 : Module.Free ℤ S]
  (n : ℕ) (x : Ideal S) (motive : (x ∈ fun I => I ∈ nonZeroDivisors (Ideal S) ∧ Ideal.absNorm I ≤ n) → Prop)
  (x_1 : x ∈ fun I => I ∈ nonZeroDivisors (Ideal S) ∧ Ideal.absNorm I ≤ n),
  (∀ (left : x ∈ nonZeroDivisors (Ideal S)) (h : Ideal.absNorm x ≤ n), motive ⋯) → motive x_1