simp only [not_and_or, not_le, not_lt] at h'
case neg
d : ℕ
I : BasicInterval
h : I.a₁ + I.b₁ ≤ d ∧ I.a₂ + I.b₂ ≤ d ∧ d < I.a₁ + I.a₂ + I.b₁ + I.b₂
h' : ¬(I.a₁ + I.b₁ ≤ Nat.succ d ∧ I.a₂ + I.b₂ ≤ Nat.succ d ∧ Nat.succ d < I.a₁ + I.a₂ + I.b₁ + I.b₂)
⊢ I.a₁ + I.b₁ ≤ Nat.succ d ∧ I.a₂ + I.b₂ ≤ Nat.succ d ∧ Nat.succ d < I.a₁ + I.a₂ + I.b₁ + I.b₂ ∨
    ((left I).a₁ + (left I).b₁ ≤ Nat.succ d ∧
        (left I).a₂ + (left I).b₂ ≤ Nat.succ d ∧ Nat.succ d < (left I).a₁ + (left I).a₂ + (left I).b₁ + (left I).b₂) ∧
      (right I).a₁ + (right I).b₁ ≤ Nat.succ d ∧
        (right I).a₂ + (right I).b₂ ≤ Nat.succ d ∧
          Nat.succ d < (right I).a₁ + (right I).a₂ + (right I).b₁ + (right I).b₂
case neg
d : ℕ
I : BasicInterval
h : I.a₁ + I.b₁ ≤ d ∧ I.a₂ + I.b₂ ≤ d ∧ d < I.a₁ + I.a₂ + I.b₁ + I.b₂
h' : Nat.succ d < I.a₁ + I.b₁ ∨ Nat.succ d < I.a₂ + I.b₂ ∨ I.a₁ + I.a₂ + I.b₁ + I.b₂ ≤ Nat.succ d
⊢ I.a₁ + I.b₁ ≤ Nat.succ d ∧ I.a₂ + I.b₂ ≤ Nat.succ d ∧ Nat.succ d < I.a₁ + I.a₂ + I.b₁ + I.b₂ ∨
    ((left I).a₁ + (left I).b₁ ≤ Nat.succ d ∧
        (left I).a₂ + (left I).b₂ ≤ Nat.succ d ∧ Nat.succ d < (left I).a₁ + (left I).a₂ + (left I).b₁ + (left I).b₂) ∧
      (right I).a₁ + (right I).b₁ ≤ Nat.succ d ∧
        (right I).a₂ + (right I).b₂ ≤ Nat.succ d ∧
          Nat.succ d < (right I).a₁ + (right I).a₂ + (right I).b₁ + (right I).b₂