proposition: Lemma int_abs_spec x : { 0 ≤ x ∧ f (int_abs Z N x) = x } + { x ≤ 0 ∧ f (int_abs Z N x) = -x }.
proof: Proof. unfold int_abs. destruct int_abs_sig as [[n E]|[n E]]. left. rewrite <-E. split. now apply to_semiring_nonneg. apply (naturals.to_semiring_unique_alt _ _). right. split. apply flip_nonpos_negate. rewrite <-E. now apply to_semiring_nonneg. rewrite <-E. now apply (naturals.to_semiring_unique_alt _ _). Qed.
imports: Coq.setoid_ring.Ring MathClasses.interfaces.naturals MathClasses.interfaces.abstract_algebra MathClasses.interfaces.orders MathClasses.orders.nat_int MathClasses.theory.integers MathClasses.theory.rings MathClasses.orders.rings