Divisibility transitivity by witnesses

import Mathlib

example (a b c : Nat) (hab : a ∣ b) (hbc : b ∣ c) : a ∣ c := by
  rcases hab with ⟨k, rfl⟩
  rcases hbc with ⟨l, rfl⟩
  exact ⟨k * l, by simp [mul_assoc]⟩