This short file gives some induction principles which deal with
the recursor and iterator on the natural numbers. For their
use in inductive proofs using deliverables see (
** Module lib_more_induction Imports lib_nat nat_iter_induction = ... : [Pred=[a:Type]a->Prop]{gamma|Type}{z|gamma}{s|gamma->gamma} {phi:Pred gamma}(phi z)->({g:gamma}(phi g)->phi (s g))-> [rec=nat_iter z s]{n:nat}phi (rec n) nat_rec_induction = ... : [Rel=[a:Type][b:Type]a->b->Prop]{gamma|Type}{z|gamma} {s|nat->gamma->gamma}{phi:Rel nat gamma}(phi zero z)-> ({m:nat}{g:gamma}(phi m g)->phi (suc m) (s m g))->[rec=nat_rec z s] {n:nat}phi n (rec n) nat_iter_induction_rev = ... : [Pred=[a:Type]a->Prop]{gamma|Type}{z|gamma}{s|gamma->gamma} {phi:Pred gamma}{n:nat}(phi (nat_iter z s n))-> ({g:gamma}(phi (s g))->phi g)->phi z