Iteration Principles

 ** Module lib_nat_iter Imports lib_nat lib_bool_funs
  nat_iter_suc = ... :
    {t|Type}{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}(Eq (lll n) n \/ is_false (f (suc (lll n))))