. apply le_sub_of_dvd_of_dvd_of_lt
  . exact Nat.dvd_mul_left _ _
  . exact h₁
  . apply Nat.lt_of_le_of_lt (m := b - 1)
    . exact Nat.div_mul_le_self _ _
    . apply tsub_lt_self h₂ zero_lt_one
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
case h₂
a b : ℕ
h₀ : 0 < a
h₂ : 0 < b
h₁ : a ∣ b
⊢ b - a ≤ (b - 1) / a * a