proposition: Lemma Z_lt_induction : forall P:Z -> Prop, (forall x:Z, (forall y:Z, 0 <= y < x -> P y) -> P x) -> forall x:Z, 0 <= x -> P x.
proof: Proof. intros; now apply Z_lt_rec. Qed.
imports: BinInt Zcompare Zorder Znat Zmisc Wf_nat