have help : ∀ i j : Fin 3, i ≤ j → i = 0 ∨ (i = j) ∨ (i = 1 ∧ j = 2)
case refine_2
d a b : ℕ
inst✝ : NeZero d
⊢ Monotone (of_fraction d a b)
case help
d a b : ℕ
inst✝ : NeZero d
⊢ ∀ (i j : Fin 3), i ≤ j → i = 0 ∨ i = j ∨ i = 1 ∧ j = 2

case refine_2
d a b : ℕ
inst✝ : NeZero d
help : ∀ (i j : Fin 3), i ≤ j → i = 0 ∨ i = j ∨ i = 1 ∧ j = 2
⊢ Monotone (of_fraction d a b)