Si x, y, z ∈ ℕ, entonces x ∣ y * x * z
Demostrar que si x, y, z ∈ N, entonces
1 |
x ∣ y * x * z |
Para ello, completar la siguiente teoría de Lean:
1 2 3 4 5 |
import data.nat.basic variables x y z : ℕ example : x ∣ y * x * z := sorry |