Require Import quotient.
Require Import Arith.

Section AbsZ.

Require Import integer.

Lemma ABSZ : ∀ z : Z, Z.

intro z.
elim (Constructive_Z_partition z).
simple induction 1.
intro.
exact (- z)%INT.
intro.
exact z.
intro.
exact z.
Defined.


Open Scope INT_scope.

Lemma ABSZ_neg : ∀ z : Z, z ≤ - 1 → ABSZ z = - z.

intros.
elim (z_lt_O z H).
intros.
unfold ABSZ in |- ×.
rewrite H0; simpl in |- ×.
auto with arith.
Qed.

Lemma ABSZ_O : ∀ z : Z, z = 0 → ABSZ z = z.

intros.
elim (z_eq_O z H).
intros.
unfold ABSZ in |- ×.
rewrite H0; simpl in |- ×.
auto with arith.
Qed.

Lemma ABSZ_pos : ∀ z : Z, 1 ≤ z → ABSZ z = z.

intros.
elim (O_lt_z z H).
intros.
unfold ABSZ in |- ×.
rewrite H0; simpl in |- ×.
auto with arith.
Qed.

Opaque ABSZ.

End AbsZ.