proposition: Lemma Z_of_nat_set : forall P:Z -> Set, (forall n:nat, P (Z.of_nat n)) -> forall x:Z, 0 <= x -> P x.
proof: Proof. intros P H x Hx. now destruct (Z_of_nat_complete_inf x Hx) as (n,->). Qed.
imports: BinInt Zcompare Zorder Znat Zmisc Wf_nat