simp_rw [mul_comm _ g, mul_assoc] at h₁ h₂
case intro
I : BasicInterval
a b g : ℕ
hg : 0 < g
h₁ : b * g * I.a₁ ≤ a * g * I.b₁
h₂ : a * g * I.b₂ ≤ b * g * I.a₂
⊢ mem a b I
case intro
I : BasicInterval
a b g : ℕ
hg : 0 < g
h₁ : g * (b * I.a₁) ≤ g * (a * I.b₁)
h₂ : g * (a * I.b₂) ≤ g * (b * I.a₂)
⊢ mem a b I