exact ⟨I'.right, h.2, hm⟩
case intro.succ.intro.intro.inr.inr
a b n✝ : ℕ
inst✝ : NeZero (Nat.succ n✝)
n : ℕ
I' : BasicInterval
hf : feasible (Nat.succ n) I'
hm✝ : mem a b I'
h : feasible (Nat.succ (Nat.succ n)) (left I') ∧ feasible (Nat.succ (Nat.succ n)) (right I')
hm : mem a b (right I')
⊢ ∃ I, feasible (Nat.succ (Nat.succ n)) I ∧ mem a b I
no goals