rintro ⟨r, ⟨ha, ha'⟩, rfl⟩
case a.mpr
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d a b : ℕ
hd : d ≠ 0
n : ℕ
⊢ (∃ a_1, (a / d < a_1 ∧ a_1 ≤ b / d) ∧ a_1 * d = n) → (a < n ∧ n ≤ b) ∧ d ∣ n
case a.mpr.intro.intro.intro
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 ∧ r * d ≤ b) ∧ d ∣ r * d