EvenOdd.agda

module EvenOdd where

open import Relation.Binary.PropositionalEquality
open import Data.Nat
open import Data.Nat.Solver
open import Data.Product

open +-*-Solver


Even : ℕ → Set
Even n = ∃[ m ] (n ≡ 2 * m) -- could use _≟_ here instead if necessary 

-- Goal: m/2 + (m/2 + zero) + (n/2 + (n/2 + zero)) ≡
--    m/2 + n/2 + (m/2 + n/2 + zero)
even+even : ∀ {m n} → Even m → Even n → Even (m + n)
even+even (m/2 , refl) (n/2 , refl) = (m/2 + n/2) , {!solve ? ?!}