proposition: Lemma Zsgn_14 : forall x : Z, (Z.sgn x <= 0)%Z -> (x <= 0)%Z.
proof: Proof. intros. case (Z_le_lt_eq_dec (Z.sgn x) 0 H). intro. apply Zlt_le_weak. apply Zsgn_11. assumption. intro. assert (x = 0%Z). apply Zsgn_2. assumption. rewrite H0. apply Z.le_refl. Qed.
imports: Coq(Lia)