Iteration Principles

 ** Module lib_nat_iter Imports lib_nat lib_bool_funs
* nat_iter_suc = ... :
    {t|SET}{z:t}{s:t->t}{n:nat}
    Eq (nat_iter z s (suc n)) (nat_iter (s z) s n)
* while_cond1 = ... :
    {f:nat->bool}[lll=nat_iter zero ([a:nat]if (f (suc a)) (suc a) a)]
    (is_true (f zero))->{n:nat}is_true (f (lll n))
* while_cond2 = ... :
    {f:nat->bool}[lll=nat_iter zero ([a:nat]if (f (suc a)) (suc a) a)]
    {n:nat}or (Eq (lll n) n) (is_false (f (suc (lll n))))