n : int_abs Z N (-f n) = n. Proof. apply (injective f). destruct (int_abs_spec (-f n)) as [[? E]|[? E]]. - symmetry. apply naturals.negate_to_ring. apply symmetry; trivial. - rewrite involutive in E. trivial. Qed.
Require Import