proposition: Lemma Zlt_0_ind : forall P:Z -> Prop, (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; now apply Zlt_0_rec. Qed.
imports: BinInt Zcompare Zorder Znat Zmisc Wf_nat