** 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))))