proposition: Lemma abs_sgn : forall n, abs n * sgn n == n.
proof: Proof. intros n. destruct_sgn n; try rewrite mul_opp_r; nzsimpl; auto. - apply abs_eq. now apply lt_le_incl. - rewrite eq_opp_l. apply abs_neq. now apply lt_le_incl. Qed.
imports: ZMulOrder