proposition: Lemma Zsgn_7 : 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). Flip. intros. simpl in |- *. reflexivity. intros. apply False_ind. apply (Z.lt_irrefl (Zneg p)). apply Z.lt_trans with 0%Z. constructor. Flip. Qed.
imports: Coq(Lia)