proposition: Lemma Zsgn_8 : forall x : Z, (x < 0)%Z -> Z.sgn x = (-1)%Z.
proof: Proof. intro. case x. intro. apply False_ind. apply (Z.lt_irrefl 0). assumption. intros. apply False_ind. apply (Z.lt_irrefl 0). apply Z.lt_trans with (Zpos p). constructor. assumption. intros. simpl in |- *. reflexivity. Qed.
imports: Coq(Lia)