rcases mem_left_or_mem_right I' hm with hm | hm
case intro.succ.intro.intro.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')
⊢ ∃ I, feasible (Nat.succ (Nat.succ n)) I ∧ mem a b I
case intro.succ.intro.intro.inr.inl
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 (left I')
⊢ ∃ I, feasible (Nat.succ (Nat.succ n)) I ∧ mem a b I

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