The predicate Even

In this section we define the predicate ``Even'', and prove some theorems characterising it.

 ** Module lib_nat_Even Imports lib_nat
  Even = ... : nat->Prop
  ev1 = ... : Even zero
  ev2 = ... : {n:nat}(Even n)->Even (suc (suc n))
  Even_elim_nondep = ... :
    {T:nat->Prop}(T zero)->({n:nat}(T n)->T (suc (suc n)))->{n:nat}
    (Even n)->T n
  Even_inv = ... :
    {n:nat}(Even n)->
    (Eq n zero \/ Ex ([x:nat](Eq n (suc (suc x)) /\ Even x)))
  Even_inv' = ... : {n:nat}(Even (suc (suc n)))->Even n