proposition: Lemma natlike_rec3 : forall P:Z -> Type, P 0 -> (forall z:Z, 0 < z -> P (Z.pred z) -> P 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. - assert (EQ : 0 <= Z.pred (Zpos p)) by now apply Z.lt_le_pred. apply Hrec. + easy. + apply IH; trivial. split; trivial. apply Z.lt_pred_l. - now destruct Hz. Qed.
imports: BinInt Zcompare Zorder Znat Zmisc Wf_nat