proposition: Lemma Z_exh : forall z : Z, (exists n : nat, z = n) \/ (exists n : nat, z = (- n)%Z).
proof: Proof. intro z. elim z. left. exists 0. auto. intro p. left. exists (nat_of_P p). rewrite convert_is_POS. reflexivity. intro p. right. exists (nat_of_P p). rewrite min_convert_is_NEG. reflexivity. Qed.
imports: Coq(Lia) CoRN.stdlib_omissions.List Coq.Logic.Eqdep_dec Coq.Setoids.Setoid