obtain ⟨⟨s₁, t₁, hcop₁, hSle, hmem₁, hne₁⟩, ⟨s₂, t₂, hcop₂, hSge, hmem₂, hne₂⟩⟩ := H
d : ℕ
inst✝ : NeZero d
I : BasicInterval
hI : feasible d I
H :
  (∃ a b, Nat.Coprime a b ∧ mem_S_le d ↑a ↑b ∧ mem a b I ∧ a * I.b₂ ≠ b * I.a₂) ∧
    ∃ a b, Nat.Coprime a b ∧ mem_S_ge d ↑a ↑b ∧ mem a b I ∧ a * I.b₁ ≠ b * I.a₁
⊢ False
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
d : ℕ
inst✝ : NeZero d
I : BasicInterval
hI : feasible d I
s₁ t₁ : ℕ
hcop₁ : Nat.Coprime s₁ t₁
hSle : mem_S_le d ↑s₁ ↑t₁
hmem₁ : mem s₁ t₁ I
hne₁ : s₁ * I.b₂ ≠ t₁ * I.a₂
s₂ t₂ : ℕ
hcop₂ : Nat.Coprime s₂ t₂
hSge : mem_S_ge d ↑s₂ ↑t₂
hmem₂ : mem s₂ t₂ I
hne₂ : s₂ * I.b₁ ≠ t₂ * I.a₁
⊢ False