apply Nat.lt_of_le_of_lt (m := b - 1)
case h₁.h₃
a b : ℕ
h₀ : 0 < a
h₂ : 0 < b
h₁ : a ∣ b
⊢ (b - 1) / a * a < b
case h₁.h₃.h₁
a b : ℕ
h₀ : 0 < a
h₂ : 0 < b
h₁ : a ∣ b
⊢ (b - 1) / a * a ≤ b - 1

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