refine ⟨?_, ?_⟩
d a b : ℕ
inst✝ : NeZero d
⊢ normalized (of_fraction d a b)
case refine_1
d a b : ℕ
inst✝ : NeZero d
⊢ of_fraction d a b 0 = 0

case refine_2
d a b : ℕ
inst✝ : NeZero d
⊢ Monotone (of_fraction d a b)