by_contra! H
d : ℕ
inst✝ : NeZero d
I : BasicInterval
hI : feasible d I
⊢ (∀ (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₁
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