by_cases h' : I.feasible d.succ
d : ℕ
I : BasicInterval
h : feasible d I
⊢ feasible (Nat.succ d) I ∨ feasible (Nat.succ d) (left I) ∧ feasible (Nat.succ d) (right I)
case pos
d : ℕ
I : BasicInterval
h : feasible d I
h' : feasible (Nat.succ d) I
⊢ feasible (Nat.succ d) I ∨ feasible (Nat.succ d) (left I) ∧ feasible (Nat.succ d) (right I)

case neg
d : ℕ
I : BasicInterval
h : feasible d I
h' : ¬feasible (Nat.succ d) I
⊢ feasible (Nat.succ d) I ∨ feasible (Nat.succ d) (left I) ∧ feasible (Nat.succ d) (right I)