refine (Nat.div_lt_iff_lt_mul ?_).mp ha
case a.mpr.intro.intro.intro.refine_1
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d a b : ℕ
hd : d ≠ 0
r : ℕ
ha : a / d < r
ha' : r ≤ b / d
⊢ a < r * d
case a.mpr.intro.intro.intro.refine_1
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d a b : ℕ
hd : d ≠ 0
r : ℕ
ha : a / d < r
ha' : r ≤ b / d
⊢ 0 < d