From 0388c440224047fea48092b6e6ba74716f993827 Mon Sep 17 00:00:00 2001
From: Pierre Roux <pierre.roux@onera.fr>
Date: Thu, 27 Jul 2023 18:28:32 +0200
Subject: [PATCH 1/2] Remove useless instance

---
 CHANGELOG_UNRELEASED.md | 5 +++++
 theories/signed.v       | 5 -----
 2 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 8a0ca059d..983909415 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -168,6 +168,11 @@
 - in `topology.v`:
   + lemma `my_ball_le` (use `ball_le` instead)
 
+- in `signed.v`:
+  + lemma `nat_snum_subproof`
+  + canonical instance `nat_snum` (useless, there is already a default instance
+    pointing to the typ_snum mechanism (then identifying nats as >= 0))
+
 ### Infrastructure
 
 ### Misc
diff --git a/theories/signed.v b/theories/signed.v
index f8e4c64f2..92a1ef1e6 100644
--- a/theories/signed.v
+++ b/theories/signed.v
@@ -925,11 +925,6 @@ Section NatStability.
 Local Open Scope nat_scope.
 Implicit Type (n : nat).
 
-Lemma nat_snum_subproof n : Signed.spec 0 ?=0 >=0 n.
-Proof. by []. Qed.
-
-Canonical nat_snum n := Signed.mk (nat_snum_subproof n).
-
 Lemma zeron_snum_subproof : Signed.spec 0 ?=0 =0 0.
 Proof. by []. Qed.
 

From e861d75889fae4b314bda90a734843386fef7a55 Mon Sep 17 00:00:00 2001
From: Pierre Roux <pierre.roux@onera.fr>
Date: Thu, 27 Jul 2023 18:41:52 +0200
Subject: [PATCH 2/2] Add signed instances for Posz and Negz

---
 CHANGELOG_UNRELEASED.md |  4 ++++
 theories/signed.v       | 20 ++++++++++++++++++++
 2 files changed, 24 insertions(+)

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 983909415..900837878 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -64,6 +64,10 @@
 - in `classical_sets.v`:
   + lemma `Zorn_bigcup`
 
+- in `signed.v`:
+  + lemmas `Posz_snum_subproof` and `Negz_snum_subproof`
+  + canonical instances `Posz_snum` and `Negz_snum`
+
 ### Changed
 
 - moved from `lebesgue_measure.v` to `real_interval.v`:
diff --git a/theories/signed.v b/theories/signed.v
index 92a1ef1e6..72ced40d8 100644
--- a/theories/signed.v
+++ b/theories/signed.v
@@ -1020,6 +1020,26 @@ Canonical maxn_snum (xnz ynz : nullity) (xr yr : reality)
 
 End NatStability.
 
+Section IntStability.
+
+Lemma Posz_snum_subproof (xnz : nullity) (xr : reality)
+    (x : {compare 0%N & xnz & xr}) :
+  Signed.spec 0%Z xnz xr (Posz x%:num).
+Proof.
+by apply/andP; split; move: xr xnz x => [[[]|]|] []//=; move=> [[|x]//= _].
+Qed.
+
+Canonical Posz_snum (xnz : nullity) (xr : reality)
+    (x : {compare 0%N & xnz & xr}) :=
+  Signed.mk (Posz_snum_subproof x).
+
+Lemma Negz_snum_subproof (n : nat) : Signed.spec 0%Z !=0 <=0 (Negz n).
+Proof. by []. Qed.
+
+Canonical Negz_snum n := Signed.mk (Negz_snum_subproof n).
+
+End IntStability.
+
 Section Morph0.
 Context {R : numDomainType} {cond : reality}.
 Local Notation nR := {num R & ?=0 & cond}.