# 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.

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.