proposition: Lemma Zlt_0_rec : forall P:Z -> Type, (forall x:Z, (forall y:Z, 0 <= y < x -> P y) -> 0 <= x -> P x) -> forall x:Z, 0 <= x -> P x.
proof: Proof. intros P Hrec x. induction x as [x IH] using (well_founded_induction_type R_wf). destruct x; intros Hx. - apply Hrec; trivial. intros y (Hy,Hy'). assert (0 < 0) by now apply Z.le_lt_trans with y. discriminate. - apply Hrec; trivial. intros y (Hy,Hy'). apply IH; trivial. now split. - now destruct Hx. Defined.
imports: BinInt Zcompare Zorder Znat Zmisc Wf_nat