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

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