x : (0 ≤ x /\ f (int_abs Z N x) = x) |_| (x ≤ 0 /\ f (int_abs Z N x) = -x). Proof. unfold int_abs. destruct (int_abs_sig Z N x) as [[n E]|[n E]]. - left. rewrite <-E. split. + eapply @to_semiring_nonneg;apply _. + apply (naturals.to_semiring_unique_alt _ _). - right. split. + apply flip_nonpos_negate. rewrite <-E. eapply @to_semiring_nonneg;apply _. + rewrite <-E. apply (naturals.to_semiring_unique_alt _ _). Qed.
Require Import