proposition: Lemma Zsgn_3 : forall x : Z, x <> 0%Z -> Z.sgn x <> 0%Z.
proof: Proof. intro x. case x. intro H. elim H. reflexivity. intros p H. simpl in |- *. discriminate. intros p H. simpl in |- *. discriminate. Qed.
imports: Coq.Arith.Compare_dec CoRN.logic.CornBasics Coq.ZArith.ZArith Coq.setoid_ring.ZArithRing Coq.Arith.Wf_nat Coq(Lia)