** Module lib_nat_div Imports lib_nat_rels lib_bool_thms
half = ... : nat->nat
even_pred = ... :
{n|nat}{b|bool}(Eq (even (suc n)) (inv b))->Eq (even n) b
half_even = ... :
{n:nat}
((is_true (even n))->Eq (times two (half n)) n /\
(is_false (even n))->Eq (suc (times two (half n))) n)