proposition: Lemma sgn_neg_iff : forall n, sgn n == -1 <-> n<0.
proof: Proof. intros n; split; try apply sgn_neg. destruct_sgn n; auto with relations. - intros. elim (lt_neq (-1) 1); auto with relations. apply lt_trans with 0. + rewrite opp_neg_pos. apply lt_0_1. + apply lt_0_1. - intros. elim (lt_neq (-1) 0); auto with relations. rewrite opp_neg_pos. apply lt_0_1. Qed.
imports: ZMulOrder