implementations.stdlib_binary_naturals

Require Import
  NArith peano_naturals theory.naturals
  abstract_algebra interfaces.naturals interfaces.orders.

Instance N_equiv : Equiv N := eq.
Instance N_0 : RingZero N := 0%N.
Instance N_1 : RingOne N := 1%N.
Instance N_plus : RingPlus N := Nplus.
Instance N_mult : RingMult N := Nmult.

Instance: SemiRing N.

Instance: x y: N, Decision (x = y) := N_eq_dec.

Instance inject_nat_N: Coerce nat N := N_of_nat.
Instance inject_N_nat: Coerce N nat := nat_of_N.

Instance: SemiRing_Morphism nat_of_N.

Instance: Inverse nat_of_N := N_of_nat.

Instance: Surjective nat_of_N.

Instance: Injective nat_of_N.

Instance: Bijective nat_of_N := {}.

Instance: Inverse N_of_nat := nat_of_N.

Instance: Bijective N_of_nat.

Instance: SemiRing_Morphism N_of_nat.

Instance: NaturalsToSemiRing N := retract_is_nat_to_sr N_of_nat.
Instance: Naturals N := retract_is_nat N_of_nat.

Instance N_le: Le N := Nle.
Instance N_lt: Lt N := Nlt.

Instance: FullPseudoSemiRingOrder N_le N_lt.

Program Instance: x y: N, Decision (x y) := λ y x,
  match Ncompare y x with
  | Gt => right _
  | _ => left _
  end.