[Agda] Confused about rewriting

[Nils Anders Danielsson]

On 2018-03-18 13:46, Philip Wadler wrote:
> So, is the proof that worked the best one, or is there a neater way to
> do it?

I suggest that you replace "2 * m" with "m * 2". Then the following
proof works:

   ∃-even : ∀ {n : ℕ} → even n → ∃[ m ] (n ≡ m * 2)
   ∃-odd  : ∀ {n : ℕ} →  odd n → ∃[ m ] (n ≡ 1 + m * 2)

   ∃-even even-zero    = zero , refl
   ∃-even (even-suc o) = map suc (cong suc) (∃-odd  o)
   ∃-odd  (odd-suc  e) = map id  (cong suc) (∃-even e)

(The map function here comes from Data.Product.)

-- 
/NAD