exact le_rfl
case refine_2.inr.inl
d a b : ℕ
inst✝ : NeZero d
help : ∀ (i j : Fin 3), i ≤ j → i = 0 ∨ i = j ∨ i = 1 ∧ j = 2
i : Fin (Nat.succ 2)
hij : i ≤ i
⊢ of_fraction d a b i ≤ of_fraction d a b i
no goals