proposition: Lemma abs_opp : forall n, abs (-n) == abs n.
proof: Proof. intros n. destruct_max n. - rewrite (abs_neq (-n)), opp_involutive. + reflexivity. + now rewrite opp_nonpos_nonneg. - rewrite (abs_eq (-n)). + reflexivity. + now rewrite opp_nonneg_nonpos. Qed.
imports: ZMulOrder