Transitividad de la divisibilidad
Demostrar con Lean4 la transitividad de la divisibilidad.
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 9 |
import Mathlib.Tactic variable {a b c : ℕ} example (divab : a ∣ b) (divbc : b ∣ c) : a ∣ c := by sorry |