proposition: Lemma natlike_rec2 : forall P:Z -> Type, P 0 -> (forall z:Z, 0 <= z -> P z -> P (Z.succ z)) -> forall z:Z, 0 <= z -> P z.
proof: Proof. intros P Ho Hrec z. induction z as [z IH] using (well_founded_induction_type R_wf). destruct z as [|p|p]; intros Hz. - apply Ho. - set (y:=Z.pred (Zpos p)). assert (LE : 0 <= y) by (unfold y; now apply Z.lt_le_pred). assert (EQ : Zpos p = Z.succ y) by (unfold y; now rewrite Z.succ_pred). rewrite EQ. apply Hrec, IH; trivial. split; trivial. unfold y; apply Z.lt_pred_l. - now destruct Hz. Qed.
imports: BinInt Zcompare Zorder Znat Zmisc Wf_nat