proposition: Lemma abs_eq_cases : forall n m, abs n == abs m -> n == m \/ n == - m.
proof: Proof. intros n m EQ. destruct (abs_or_opp_abs n) as [EQn|EQn]. - rewrite EQn, EQ. apply abs_eq_or_opp. - rewrite EQn, EQ, opp_inj_wd, eq_opp_l, or_comm. apply abs_eq_or_opp. Qed.
imports: ZMulOrder