proposition: Lemma sgn_mul : forall n m, sgn (n*m) == sgn n * sgn m.
proof: Proof. intros n m. destruct_sgn n; nzsimpl. - destruct_sgn m. + apply sgn_pos. now apply mul_pos_pos. + apply sgn_null. rewrite eq_mul_0; auto with relations. + apply sgn_neg. now apply mul_pos_neg. - apply sgn_null. rewrite eq_mul_0; auto with relations. - destruct_sgn m; try rewrite mul_opp_opp; nzsimpl. + apply sgn_neg. now apply mul_neg_pos. + apply sgn_null. rewrite eq_mul_0; auto with relations. + apply sgn_pos. now apply mul_neg_neg. Qed.
imports: ZMulOrder