x : int_abs Z N x = 0 <-> x = 0. Proof. split; intros E1. - destruct (int_abs_spec x) as [[_ E2]|[_ E2]];[|apply flip_negate_0]; rewrite <-E2, E1, (preserves_0 (f:=f)); trivial. - rewrite E1, <-(preserves_0 (f:=f)). apply int_abs_nat. Qed.
Require Import