exact ⟨Nat.le_of_mul_le_mul_left h₁ hg, Nat.le_of_mul_le_mul_left h₂ hg⟩
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
no goals