<html>
<head>
<meta http-equiv="content-type" content="text/html; charset=UTF-8">
</head>
<body text="#000000" bgcolor="#FFFFFF">
Assuming a predicate <i>even</i><br>
<p><b>data even : ℕ -> Set where</b><b><br>
</b><b> even0 : even zero</b><b><br>
</b><b> even1 : even (suc zero)</b><b><br>
</b><b> evenSS : {n : ℕ} -> even n -> even (suc (suc n))</b></p>
<p>I would like to prove:</p>
<p><b>inversionEven : {n : ℕ} -> even (suc (suc n)) -> even n</b></p>
<p>In Coq, I could use <br>
</p>
<ul>
<li>either a command <i>inversion</i></li>
<li>or a somewhat direct proof<i> </i>that applies even_ind. </li>
</ul>
<p>Are there similar features in Agda ?<br>
</p>
<pre class="moz-signature" cols="72">--
Cheers
---------------------------
Pierre Lescanne (Emeritus Professor)
LIP / École normale supérieure de Lyon
46 allée d'Italie
69364 LYON Cedex 07, France
tél: +33 6 85 70 94 31
<a class="moz-txt-link-freetext" href="http://perso.ens-lyon.fr/pierre.lescanne/">http://perso.ens-lyon.fr/pierre.lescanne/</a>
---------------------------
</pre>
</body>
</html>