proposition: Lemma sgn_opp : forall n, sgn (-n) == - sgn n.
proof: Proof. intros n. destruct_sgn n. - apply sgn_neg. now rewrite opp_neg_pos. - setoid_replace n with 0 by auto with relations. rewrite opp_0. apply sgn_0. - rewrite opp_involutive. apply sgn_pos. now rewrite opp_pos_neg. Qed.
imports: ZMulOrder