proposition: Lemma CZ_exh : forall z : Z, {n : nat | z = n} or {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.Arith.Compare_dec CoRN.logic.CornBasics Coq.ZArith.ZArith Coq.setoid_ring.ZArithRing Coq.Arith.Wf_nat Coq(Lia)