%Every natural number is either even or odd

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.