obtain ⟨n, rfl⟩ := Nat.exists_eq_succ_of_ne_zero (NeZero.ne d)
d a b : ℕ
inst✝ : NeZero d
⊢ ∃ I, feasible d I ∧ mem a b I
case intro
a b n : ℕ
inst✝ : NeZero (Nat.succ n)
⊢ ∃ I, feasible (Nat.succ n) I ∧ mem a b I