proposition: Lemma Zsgn_1 : forall x : Z, {Z.sgn x = 0%Z} + {Z.sgn x = 1%Z} + {Z.sgn x = (-1)%Z}.
proof: Proof. intro x. case x. left. left. unfold Z.sgn in |- *. reflexivity. intro p. simpl in |- *. left. right. reflexivity. intro p. right. simpl in |- *. reflexivity. Qed.
imports: Coq.Arith.Compare_dec CoRN.logic.CornBasics Coq.ZArith.ZArith Coq.setoid_ring.ZArithRing Coq.Arith.Wf_nat Coq(Lia)