implementations.nonneg_integers_naturals

Require
  peano_naturals orders.integers theory.integers.
Require Import
  Ring RelationClasses
  abstract_algebra interfaces.integers interfaces.naturals interfaces.orders
  interfaces.additional_operations int_abs.
Require Export
  implementations.nonneg_semiring_elements.

Section nonneg_integers_naturals.
Context Z `{Integers Z} `{Apart Z} `{!TrivialApart Z} `{!FullPseudoSemiRingOrder Zle Zlt}.

Add Ring Z: (rings.stdlib_ring_theory Z).

Program Definition of_nat (x : nat) : Z⁺ := (naturals_to_semiring nat Z x)↾_.

Local Ltac unfold_equivs := unfold equiv, sig_equiv in *; simpl in *.

Instance: Proper ((=) ==> (=)) of_nat.

Instance: SemiRing_Morphism of_nat.

Program Instance to_nat: Inverse of_nat := λ x, int_abs Z nat (`x).

Instance: Proper ((=) ==> (=)) to_nat.

Instance ZPos_to_nat_sr_morphism: SemiRing_Morphism to_nat.

Instance: Surjective of_nat.

Global Instance: NaturalsToSemiRing (Z⁺) := naturals.retract_is_nat_to_sr of_nat.
Global Instance: Naturals (Z⁺) := naturals.retract_is_nat of_nat.

Global Program Instance ZPos_cut_minus `{ x y : Z, Decision (x y)} : CutMinus (Z⁺)
  := λ x y, if decide_rel (≤) x y then 0 else (x - y)↾_.

Global Instance: CutMinusSpec (Z⁺) ZPos_cut_minus.
End nonneg_integers_naturals.