<div dir="ltr">Thanks, Nils! I had spotted that I should avoid 2 * m + 1 and instead write 1 + 2 *m, but not that 1 + m * 2 eliminates the need for my lemma. Cheers! -- P</div><div class="gmail_extra"><br clear="all"><div><div class="gmail_signature" data-smartmail="gmail_signature"><div dir="ltr"><div><div dir="ltr">.   \ Philip Wadler, Professor of Theoretical Computer Science,<br>.   /\ School of Informatics, University of Edinburgh<br></div><div>.  /  \ and Senior Research Fellow, IOHK<br></div><div dir="ltr">. <span><a href="http://homepages.inf.ed.ac.uk/wadler/" target="_blank">http://homepages.inf.ed.ac.uk/wadler/</a></span></div></div></div></div></div>
<br><div class="gmail_quote">On 20 March 2018 at 07:53, Nils Anders Danielsson <span dir="ltr"><<a href="mailto:nad@cse.gu.se" target="_blank">nad@cse.gu.se</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><span class="">On 2018-03-18 13:46, Philip Wadler wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
So, is the proof that worked the best one, or is there a neater way to<br>
do it?<br>
</blockquote>
<br></span>
I suggest that you replace "2 * m" with "m * 2". Then the following<br>
proof works:<br>
<br>
  ∃-even : ∀ {n : ℕ} → even n → ∃[ m ] (n ≡ m * 2)<br>
  ∃-odd  : ∀ {n : ℕ} →  odd n → ∃[ m ] (n ≡ 1 + m * 2)<br>
<br>
  ∃-even even-zero    = zero , refl<br>
  ∃-even (even-suc o) = map suc (cong suc) (∃-odd  o)<br>
  ∃-odd  (odd-suc  e) = map id  (cong suc) (∃-even e)<br>
<br>
(The map function here comes from Data.Product.)<span class="HOEnZb"><font color="#888888"><br>
<br>
-- <br>
/NAD<br>
<br>
</font></span></blockquote></div><br></div>