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