El producto por un par es par
Demostrar que los productos de los números naturales por números pares son pares.
Para ello, completar la siguiente teoría de Lean:
|
1 2 3 4 5 6 7 |
import data.nat.parity import tactic open nat example : ∀ m n : ℕ, even n → even (m * n) := sorry |