proposition: Lemma Zsgn_12 : forall x : Z, (0 < Z.sgn x)%Z -> (0 < x)%Z.
proof: Proof. intros. apply Zsgn_9. case (Zsgn_1' x). intro. case s. intro. generalize (Zorder.Zlt_not_eq _ _ H). intro. generalize (sym_eq e). intro. apply False_ind. apply (H0 H1). trivial. intro. rewrite e in H. generalize (Zorder.Zlt_not_eq _ _ H). intro. apply False_ind. discriminate. Qed.
imports: Coq(Lia)