proposition: Lemma Zsgn_9 : forall x : Z, Z.sgn x = 1%Z -> (0 < x)%Z.
proof: Proof. intro. case x. intro. apply False_ind. simpl in H. discriminate. intros. constructor. intros. apply False_ind. discriminate. Qed.
imports: Coq(Lia)