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