proposition: Lemma Z_to_nat_correct:forall (z:Z)(H:(0<=z)%Z), z=(Z_of_nat (Z_to_nat H)).
proof: Proof. intro z. case z. intro H. unfold Z_to_nat. reflexivity. intros p H. unfold Z_to_nat. cut ( Z_of_nat (nat_of_P p)= Zpos p). intuition. apply inject_nat_convert. intros p H. cut False. intuition. intuition. Qed.
imports: Coq(Lia) CoRN.stdlib_omissions.List Coq.Logic.Eqdep_dec Coq.Setoids.Setoid