rewrite [add_tsub_assoc_of_le (Nat.one_le_of_lt h₀)]
case h₂
a b : ℕ
h₀ : 0 < a
h₂ : 0 < b
h₁ : a ∣ b
⊢ b ≤ (b + a - 1) / a * a
case h₂
a b : ℕ
h₀ : 0 < a
h₂ : 0 < b
h₁ : a ∣ b
⊢ b ≤ (b + (a - 1)) / a * a