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