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