. exact h₁
case h₁.h₂
a b : ℕ
h₀ : 0 < a
h₂ : 0 < b
h₁ : a ∣ b
⊢ a ∣ b

case h₁.h₃
a b : ℕ
h₀ : 0 < a
h₂ : 0 < b
h₁ : a ∣ b
⊢ (b - 1) / a * a < b
case h₁.h₃
a b : ℕ
h₀ : 0 < a
h₂ : 0 < b
h₁ : a ∣ b
⊢ (b - 1) / a * a < b