Merge pull request #996 from proux01/int_signed_instances

Int signed instances

CHANGELOG_UNRELEASED.md

@@ -96,6 +96,10 @@
 - in `topology.v`:
   + lemma `closed_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`:
@@ -220,6 +224,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

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.
 
@@ -1025,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}.