From b3d3d9c27c8ea0e401b82fc485939debc02335ea Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sat, 22 Apr 2023 20:01:03 +0200
Subject: [PATCH] Also put results about `N` in a module.

---
 stdpp/numbers.v | 44 ++++++++++++++++++++++++--------------------
 1 file changed, 24 insertions(+), 20 deletions(-)

diff --git a/stdpp/numbers.v b/stdpp/numbers.v
index a9427ae8..8e653c99 100644
--- a/stdpp/numbers.v
+++ b/stdpp/numbers.v
@@ -355,28 +355,32 @@ Infix "`min`" := N.min (at level 35) : N_scope.
 
 Global Arguments N.add : simpl never.
 
-Global Instance Npos_inj : Inj (=) (=) Npos.
-Proof. by injection 1. Qed.
+Global Hint Extern 0 (_ ≤ _)%N => reflexivity : core.
 
-Global Instance N_eq_dec: EqDecision N := N.eq_dec.
-Global Program Instance N_le_dec : RelDecision N.le := λ x y,
-  match N.compare x y with Gt => right _ | _ => left _ end.
-Solve Obligations with naive_solver.
-Global Program Instance N_lt_dec : RelDecision N.lt := λ x y,
-  match N.compare x y with Lt => left _ | _ => right _ end.
-Solve Obligations with naive_solver.
-Global Instance N_inhabited: Inhabited N := populate 1%N.
-Global Instance N_lt_pi x y : ProofIrrel (x < y)%N.
-Proof. unfold N.lt. apply _. Qed.
-
-Global Instance N_le_po: PartialOrder (≤)%N.
-Proof.
-  repeat split; red; [apply N.le_refl | apply N.le_trans | apply N.le_antisymm].
-Qed.
-Global Instance N_le_total: Total (≤)%N.
-Proof. repeat intro; lia. Qed.
+Module N.
+  Export BinNat.N.
 
-Global Hint Extern 0 (_ ≤ _)%N => reflexivity : core.
+  Global Instance pos_inj : Inj (=) (=) N.pos.
+  Proof. by injection 1. Qed.
+
+  Global Instance eq_dec : EqDecision N := N.eq_dec.
+  Global Program Instance le_dec : RelDecision N.le := λ x y,
+    match N.compare x y with Gt => right _ | _ => left _ end.
+  Solve Obligations with naive_solver.
+  Global Program Instance lt_dec : RelDecision N.lt := λ x y,
+    match N.compare x y with Lt => left _ | _ => right _ end.
+  Solve Obligations with naive_solver.
+  Global Instance inhabited : Inhabited N := populate 1%N.
+  Global Instance lt_pi x y : ProofIrrel (x < y)%N.
+  Proof. unfold N.lt. apply _. Qed.
+
+  Global Instance le_po : PartialOrder (≤)%N.
+  Proof.
+    repeat split; red; [apply N.le_refl | apply N.le_trans | apply N.le_antisymm].
+  Qed.
+  Global Instance le_total : Total (≤)%N.
+  Proof. repeat intro; lia. Qed.
+End N.
 
 (** * Notations and properties of [Z] *)
 Local Open Scope Z_scope.
-- 
GitLab