[Agda] inversion

[Pierre Lescanne (en)]

Assuming a predicate /even/

*data even :  ℕ -> Set where**
**  even0 : even zero**
**  even1 : even (suc zero)**
**  evenSS : {n : ℕ} -> even n -> even (suc (suc n))*

I would like to prove:

*inversionEven : {n : ℕ} -> even (suc (suc n)) -> even n*

In Coq, I could use

  * either a command /inversion/
  * or a somewhat direct proof//that applies even_ind.

Are there similar features in Agda ?

-- 
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
http://perso.ens-lyon.fr/pierre.lescanne/
---------------------------

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20190219/f5333680/attachment.html>