proposition: Lemma abs_max : forall n, abs n == max n (-n).
proof: Proof. intros n. destruct_max n. - rewrite max_l; auto with relations. apply le_trans with 0; auto. rewrite opp_nonpos_nonneg; auto. - rewrite max_r; auto with relations. apply le_trans with 0; auto. rewrite opp_nonneg_nonpos; auto. Qed.
imports: ZMulOrder