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 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.
imports: HoTT.Classes.interfaces.naturals HoTT.Classes.interfaces.abstract_algebra HoTT.Classes.interfaces.orders HoTT.Classes.orders.nat_int HoTT.Classes.theory.integers HoTT.Classes.theory.rings HoTT.Classes.theory.groups HoTT.Classes.orders.rings