proposition: Lemma natgen_ind : forall P : Z -> Prop, (forall x : Z, (0 <= x)%Z -> (forall y : Z, (0 <= y)%Z -> (y < x)%Z -> P y) -> P x) -> forall x : Z, (0 <= x)%Z -> P x.
proof: Proof. intros; apply Z_of_nat_prop. intro; apply recur2 with (P := fun n : nat => P (Z_of_nat n)). intros; apply H. omega. intro; intro; apply Z_of_nat_prop with (P := fun y : Z => (y < Z_of_nat n0)%Z -> P y). intros; apply H1; omega. trivial. trivial. Qed.
imports: ZArith Omega