proposition: Theorem Zabs_absolu : forall z : Z, Z.abs z = Z_of_nat (Z.abs_nat z).
proof: Proof. intros z; case z; simpl in |- *; auto; intros p; apply sym_equal; apply inject_nat_convert; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz