proposition: Lemma Zsgn_3 : forall x : Z, x <> 0%Z -> Z.sgn x <> 0%Z.
proof: Proof. intro. case x. intros. apply False_ind. apply H. reflexivity. intros. simpl in |- *. discriminate. intros. simpl in |- *. discriminate. Qed.
imports: Coq(Lia)