. rewrite [tsub_le_iff_right]
  rewrite [← Nat.succ_mul]
  rewrite [← Nat.add_div_right _ h₀]
  rewrite [tsub_add_eq_add_tsub (Nat.one_le_of_lt h₂)]
  rewrite [add_tsub_assoc_of_le (Nat.one_le_of_lt h₀)]
  trans b / a * a
  . rw [Nat.div_mul_cancel h₁]
  . apply Nat.mul_le_mul_right
    apply Nat.div_le_div_right
    exact Nat.le_add_right _ _
case h₂
a b : ℕ
h₀ : 0 < a
h₂ : 0 < b
h₁ : a ∣ b
⊢ b - a ≤ (b - 1) / a * a
no goals