simp only [mem, mem_interior] at h ⊢
a b : ℕ
I : BasicInterval
h : mem_interior a b I
⊢ mem a b I
a b : ℕ
I : BasicInterval
h : b * I.a₁ < a * I.b₁ ∧ a * I.b₂ < b * I.a₂
⊢ b * I.a₁ ≤ a * I.b₁ ∧ a * I.b₂ ≤ b * I.a₂