x : 0 ≤ x -> f (int_abs Z N x) = x. Proof. intros E1. destruct (int_abs_spec x) as [[n E2]|[n E2]];trivial. assert (Hrw : x = 0). - apply (antisymmetry (<=));trivial. - rewrite Hrw,int_abs_0, (preserves_0 (f:=f)). trivial. Qed.
Require Import