constructor
case a
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d a b : ℕ
hd : d ≠ 0
n : ℕ
⊢ (a < n ∧ n ≤ b) ∧ d ∣ n ↔ ∃ a_1, (a / d < a_1 ∧ a_1 ≤ b / d) ∧ a_1 * d = n
case a.mp
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d a b : ℕ
hd : d ≠ 0
n : ℕ
⊢ (a < n ∧ n ≤ b) ∧ d ∣ n → ∃ a_2, (a / d < a_2 ∧ a_2 ≤ b / d) ∧ a_2 * d = n

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