proposition: Lemma Zsgn_1' : forall x : Z, {Z.sgn x = 0%Z} + {Z.sgn x = 1%Z} + {Z.sgn x = (-1)%Z}.
proof: Proof. intros. case x. left. left. unfold Z.sgn in |- *. reflexivity. intro. simpl in |- *. left. right. reflexivity. intro. right. simpl in |- *. reflexivity. Qed.
imports: Coq(Lia)