proposition: Lemma abs_spec : forall n, (0 <= n /\ abs n == n) \/ (n < 0 /\ abs n == -n).
proof: Proof. intros n. destruct (le_gt_cases 0 n). - left; split; auto. now apply abs_eq. - right; split; auto. apply abs_neq. now apply lt_le_incl. Qed.
imports: ZMulOrder