https://www.glc.us.es/~jalonso/calculemus/10-jul-23/
∀ m n : ℕ, Even n → Even (m * n)