Every natural number is either even or odd

even-or-odd.lf

nat : type.
z : nat.
s : {x:nat} nat.
 
even : {N:nat} type.
odd : {N:nat} type.
even-z : even z.
even-s : {N:nat}{O: odd N} even (s N).
odd-s : {N:nat}{E: even N} odd (s N).

even-or-odd.ath

Specification "even-or-odd.lf".
 
Theorem even-or-odd :
  forall N, {N : nat} => (exists D, {D : even N}) \/ (exists D, {D : odd N}).
induction on 1. intros. case H1.
  %case 1: N = (s x)
    apply IH to H2. case H3.
      %case 1.1: even x
        right. exists (odd-s x D). search.
      %case 1.2: odd x
        left. exists (even-s x D). search.
  %case 2: N = z
    left. exists even-z. search.