. rw [Nat.div_mul_cancel h₁]
a b : ℕ
h₀ : 0 < a
h₂ : 0 < b
h₁ : a ∣ b
⊢ b ≤ b / a * a

a b : ℕ
h₀ : 0 < a
h₂ : 0 < b
h₁ : a ∣ b
⊢ b / a * a ≤ (b + (a - 1)) / a * a
a b : ℕ
h₀ : 0 < a
h₂ : 0 < b
h₁ : a ∣ b
⊢ b / a * a ≤ (b + (a - 1)) / a * a