exact ⟨I.a₂, I.b₂, hI.2.1, H⟩
case inr.intro.intro.inr
d : ℕ
inst✝ : NeZero d
a b : ℕ
h : d < a + b
I : BasicInterval
hI : feasible d I
hIab : mem a b I
hab : a ≠ 0 ∨ b ≠ 0
H : of_fraction d I.a₂ I.b₂ ≤ of_fraction d a b
⊢ ∃ s t, s + t ≤ d ∧ of_fraction d s t ≤ of_fraction d a b
no goals