diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 70a6cb529..0b8d15761 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -56,6 +56,8 @@
 
 ### Deprecated
 
+- file `signed.v` (use `itv.v` instead)
+
 - in `itv.v`:
   + notation `%:inum` (use `%:num` instead)
 
diff --git a/analysis_stdlib/Rstruct_topology.v b/analysis_stdlib/Rstruct_topology.v
index 1d8e3f65a..ce19bb01e 100644
--- a/analysis_stdlib/Rstruct_topology.v
+++ b/analysis_stdlib/Rstruct_topology.v
@@ -12,7 +12,7 @@ From mathcomp Require Import archimedean.
 From HB Require Import structures.
 From mathcomp Require Import mathcomp_extra.
 From mathcomp Require Import boolp classical_sets.
-From mathcomp Require Import reals signed.
+From mathcomp Require Import reals itv.
 From mathcomp Require Import topology.
 From mathcomp Require Export Rstruct.
 
diff --git a/analysis_stdlib/showcase/uniform_bigO.v b/analysis_stdlib/showcase/uniform_bigO.v
index 58e6e9c5b..80306f9dd 100644
--- a/analysis_stdlib/showcase/uniform_bigO.v
+++ b/analysis_stdlib/showcase/uniform_bigO.v
@@ -3,7 +3,7 @@ From Coq Require Import Reals.
 From Coq Require Import ssreflect ssrfun ssrbool.
 From mathcomp Require Import ssrnat eqtype choice fintype bigop order ssralg ssrnum.
 From mathcomp Require Import boolp reals Rstruct_topology ereal.
-From mathcomp Require Import classical_sets signed topology normedtype landau.
+From mathcomp Require Import classical_sets itv topology normedtype landau.
 
 Set Implicit Arguments.
 Unset Strict Implicit.
@@ -98,7 +98,7 @@ Proof.
 move=> fOg; apply/Ouex_to_P; move: fOg => /eqOP [k [kreal hk]].
 have /hk [Q [->]] : k < maxr 1 (k + 1) by rewrite lt_max ltrDl orbC ltr01.
 move=> [R [[_/posnumP[e1] Re1] [_/posnumP[e2] Re2]] sRQ] fOg.
-exists (minr e1%:num e2%:num) => //.
+exists (minr e1%:num e2%:num); first by apply: gt0; exact: RbaseSymbolsImpl.R.
 exists (maxr 1 (k + 1)); first by rewrite lt_max ltr01.
 move=> x dx dxe Pdx; apply: (fOg (x, dx)); split=> //=.
 move: dxe; rewrite gt_max !lt_min => /andP[/andP [dxe11 _] /andP [_ dxe22]].
diff --git a/reals/all_reals.v b/reals/all_reals.v
index 1f7707f6c..00cdd1bfb 100644
--- a/reals/all_reals.v
+++ b/reals/all_reals.v
@@ -1,4 +1,3 @@
-From mathcomp Require Export signed.
 From mathcomp Require Export itv.
 From mathcomp Require Export constructive_ereal.
 From mathcomp Require Export reals.
diff --git a/reals/constructive_ereal.v b/reals/constructive_ereal.v
index 6caabc258..68141caa2 100644
--- a/reals/constructive_ereal.v
+++ b/reals/constructive_ereal.v
@@ -11,7 +11,7 @@
    bounds of intervals*)
 From HB Require Import structures.
 From mathcomp Require Import all_ssreflect all_algebra finmap.
-From mathcomp Require Import mathcomp_extra signed.
+From mathcomp Require Import mathcomp_extra itv.
 
 (**md**************************************************************************)
 (* # Extended real numbers $\overline{R}$                                     *)
@@ -3462,201 +3462,689 @@ Module ConstructiveDualAddTheory.
 Export DualAddTheory.
 End ConstructiveDualAddTheory.
 
-Definition posnume (R : numDomainType) of phant R := {> 0 : \bar R}.
-Notation "{ 'posnum' '\bar' R }" := (@posnume _ (Phant R)) : type_scope.
-Definition nonnege (R : numDomainType) of phant R := {>= 0 : \bar R}.
-Notation "{ 'nonneg' '\bar' R }" := (@nonnege _ (Phant R)) : type_scope.
+Section Itv.
+Context {R : numDomainType}.
 
-Notation "x %:pos" := (widen_signed x%:sgn : {posnum \bar _}) (only parsing)
-  : ereal_dual_scope.
-Notation "x %:pos" := (widen_signed x%:sgn : {posnum \bar _}) (only parsing)
-  : ereal_scope.
-Notation "x %:nng" := (widen_signed x%:sgn : {nonneg \bar _}) (only parsing)
-  : ereal_dual_scope.
-Notation "x %:nng" := (widen_signed x%:sgn : {nonneg \bar _}) (only parsing)
-  : ereal_scope.
-Notation "x %:pos" := (@widen_signed ereal_display _ _ _ _
-    (@Signed.from _ _ _ _ _ _ (Phantom _ x))
-    !=0 (KnownSign.Real (KnownSign.Sign >=0)) _ _)
-  (only printing) : ereal_dual_scope.
-Notation "x %:pos" := (@widen_signed ereal_display _ _ _ _
-    (@Signed.from _ _ _ _ _ _ (Phantom _ x))
-    !=0 (KnownSign.Real (KnownSign.Sign >=0)) _ _)
-  (only printing) : ereal_scope.
-Notation "x %:nng" := (@widen_signed ereal_display _ _ _ _
-    (@Signed.from _ _ _ _ _ _ (Phantom _ x))
-    ?=0 (KnownSign.Real (KnownSign.Sign >=0)) _ _)
-  (only printing) : ereal_dual_scope.
-Notation "x %:nng" := (@widen_signed ereal_display _ _ _ _
-    (@Signed.from _ _ _ _ _ _ (Phantom _ x))
-    ?=0 (KnownSign.Real (KnownSign.Sign >=0)) _ _)
-  (only printing) : ereal_scope.
+Definition ext_num_sem (i : interval int) (x : \bar R) :=
+  (0 >=< x)%O
+  && let: Interval l u := i in
+     x \in Interval (Itv.map_itv_bound (EFin \o intr) l)
+             (Itv.map_itv_bound (EFin \o intr) u).
 
-#[global] Hint Extern 0 (is_true (0%E < _)%O) => solve [apply: gt0] : core.
-#[global] Hint Extern 0 (is_true (_ < 0%E)%O) => solve [apply: lt0] : core.
-#[global] Hint Extern 0 (is_true (0%E <= _)%O) => solve [apply: ge0] : core.
-#[global] Hint Extern 0 (is_true (_ <= 0%E)%O) => solve [apply: le0] : core.
-#[global] Hint Extern 0 (is_true (0%E >=< _)%O) => solve [apply: cmp0] : core.
-#[global] Hint Extern 0 (is_true (_ != 0%E)%O) => solve [apply: neq0] : core.
+Local Notation num_spec := (Itv.spec (@Itv.num_sem _)).
+Local Notation num_def R := (Itv.def (@Itv.num_sem R)).
+Local Notation num_itv_bound R := (@Itv.map_itv_bound _ R intr).
 
-Section SignedNumDomainStability.
-Context {R : numDomainType}.
+Local Notation ext_num_spec := (Itv.spec ext_num_sem).
+Local Notation ext_num_def := (Itv.def ext_num_sem).
+Local Notation ext_num_itv_bound :=
+  (@Itv.map_itv_bound _ (\bar R) (EFin \o intr)).
+
+Lemma ext_num_num_sem_subproof i (x : R) :
+  Itv.ext_num_sem i x%:E = Itv.num_sem i x.
+Proof. by case: i => [l u]; do 2![congr (_ && _)]; [case: l | case: u]. Qed.
+
+Lemma ext_num_num_spec_subproof i (x : R) :
+  ext_num_spec i x%:E = num_spec i x.
+Proof. by case: i => [//| i]; apply: ext_num_num_sem_subproof. Qed.
+
+Lemma EFin_le_map_itv_bound (x y : itv_bound R) :
+  (Itv.map_itv_bound EFin x <= Itv.map_itv_bound EFin y)%O = (x <= y)%O.
+Proof. by case: x y => [xb x | x] [yb y | y]. Qed.
+
+Lemma EFin_BLeft_le_map_itv_bound (x : itv_bound R) (y : R) :
+  (Itv.map_itv_bound EFin x <= BLeft y%:E)%O = (x <= BLeft y)%O.
+Proof.
+rewrite -[BLeft y%:E]/(Itv.map_itv_bound EFin (BLeft y)).
+by rewrite EFin_le_map_itv_bound.
+Qed.
+
+Lemma BRight_EFin_le_map_itv_bound (x : R) (y : itv_bound R) :
+  (BRight x%:E <= Itv.map_itv_bound EFin y)%O = (BRight x <= y)%O.
+Proof.
+rewrite -[BRight x%:E]/(Itv.map_itv_bound EFin (BRight x)).
+by rewrite EFin_le_map_itv_bound.
+Qed.
+
+Lemma ext_le_map_itv_bound (x y : itv_bound int) :
+  (ext_num_itv_bound x <= ext_num_itv_bound y)%O = (x <= y)%O.
+Proof.
+rewrite !(map_itv_bound_comp EFin intr)/=.
+by rewrite EFin_le_map_itv_bound intr_le_map_itv_bound.
+Qed.
+
+Lemma subitv_map_itv (x y : Itv.t) : Itv.sub x y ->
+  forall z : \bar R, ext_num_spec x z -> ext_num_spec y z.
+Proof.
+case: x y => [| x] [| y] //= x_sub_y z /andP[rz]; rewrite /Itv.ext_num_sem rz/=.
+move: x y x_sub_y => [lx ux] [ly uy] /andP[lel leu] /=.
+move=> /andP[lxz zux]; apply/andP; split.
+- by apply: le_trans lxz; rewrite ext_le_map_itv_bound.
+- by apply: le_trans zux _; rewrite ext_le_map_itv_bound.
+Qed.
+
+Section ItvTheory.
+Context {i : Itv.t}.
+Implicit Type x : ext_num_def i.
+
+Lemma ext_widen_itv_subproof x i' : Itv.sub i i' ->
+  ext_num_spec i' x%:inum.
+Proof. by case: x => x /= /[swap] /subitv_map_itv; apply. Qed.
+
+Definition ext_widen_itv x i' (uni : unify_itv i i') :=
+  Itv.mk (ext_widen_itv_subproof x uni).
+
+Lemma gt0e x : unify_itv i (Itv.Real `]Posz 0, +oo[) -> 0%E < x%:inum :> \bar R.
+Proof.
+case: x => x /= /[swap] /subitv_map_itv /[apply] /andP[_].
+by rewrite /= in_itv/= andbT.
+Qed.
+
+Lemma lte0 x : unify_itv i (Itv.Real `]-oo, Posz 0[) -> x%:inum < 0%E :> \bar R.
+Proof.
+by case: x => x /= /[swap] /subitv_map_itv /[apply] /andP[_] /=; rewrite in_itv.
+Qed.
+
+Lemma ge0e x : unify_itv i (Itv.Real `[Posz 0, +oo[) -> 0%E <= x%:inum :> \bar R.
+Proof.
+case: x => x /= /[swap] /subitv_map_itv /[apply] /andP[_] /=.
+by rewrite in_itv/= andbT.
+Qed.
+
+Lemma lee0 x : unify_itv i (Itv.Real `]-oo, Posz 0]) -> x%:inum <= 0%E :> \bar R.
+Proof.
+by case: x => x /= /[swap] /subitv_map_itv /[apply] /andP[_] /=; rewrite in_itv.
+Qed.
+
+Lemma cmp0e x : unify_itv i (Itv.Real `]-oo, +oo[) -> (0%E >=< x%:inum)%O.
+Proof. by case: i x => [//| [l u] [[x||//] /=/andP[/= xr _]]]. Qed.
+
+Lemma neqe0 x :
+  unify (fun ix iy => negb (Itv.sub ix iy)) (Itv.Real `[0%Z, 0%Z]) i ->
+  x%:inum != 0 :> \bar R.
+Proof.
+case: i x => [//| [l u] [x /= Px]]; apply: contra => /eqP x0 /=.
+move: Px; rewrite x0 => /and3P[_ /= l0 u0]; apply/andP; split.
+- by case: l l0 => [[] l |]; rewrite ?bnd_simp ?lee_fin ?lte_fin ?lerz0 ?ltrz0.
+- by case: u u0 => [[] u |]; rewrite ?bnd_simp ?lee_fin ?lte_fin ?ler0z ?ltr0z.
+Qed.
+
+End ItvTheory.
+
+Lemma pinfty_inum_subproof : ext_num_spec (Itv.Real `]1%Z, +oo[) (+oo : \bar R).
+Proof. by apply/and3P; rewrite /= cmp0y !bnd_simp real_ltry. Qed.
+
+Canonical pinfty_inum := Itv.mk (pinfty_inum_subproof).
+
+Lemma ninfty_inum_subproof :
+  ext_num_spec (Itv.Real `]-oo, (-1)%Z[) (-oo : \bar R).
+Proof. by apply/and3P; rewrite /= cmp0Ny !bnd_simp real_ltNyr. Qed.
+
+Canonical ninfty_snum := Itv.mk (ninfty_inum_subproof).
+
+Lemma EFin_inum_subproof i (x : num_def R i) : ext_num_spec i x%:num%:E.
+Proof.
+case: i x => [//| [l u] [x /=/and3P[xr /= lx xu]]].
+by apply/and3P; split=> [//||]; [case: l lx | case: u xu].
+Qed.
+
+Canonical EFin_inum i (x : num_def R i) := Itv.mk (EFin_inum_subproof x).
+
+Definition keep_nonneg_itv_bound_subdef b :=
+  match b with
+  | BSide _ (Posz _) => BLeft 0%Z
+  | BSide _ (Negz _) => -oo%O
+  | BInfty _ => -oo%O
+  end.
+Arguments keep_nonneg_itv_bound_subdef /.
 
-Lemma pinfty_snum_subproof : Signed.spec 0 !=0 >=0 (+oo : \bar R).
-Proof. by rewrite /= le0y. Qed.
+Definition keep_nonpos_itv_bound_subdef b :=
+  match b with
+  | BSide _ (Negz _) | BSide _ (Posz 0) => BRight 0%Z
+  | BSide _ (Posz (S _)) => +oo%O
+  | BInfty _ => +oo%O
+  end.
+Arguments keep_nonpos_itv_bound_subdef /.
 
-Canonical pinfty_snum := Signed.mk (pinfty_snum_subproof).
+Definition fine_itv_subdef i :=
+  let: Interval l u := i in
+  Interval (keep_nonneg_itv_bound_subdef l) (keep_nonpos_itv_bound_subdef u).
 
-Lemma ninfty_snum_subproof : Signed.spec 0 !=0 <=0 (-oo : \bar R).
-Proof. by rewrite /= leNy0. Qed.
+Lemma fine_inum_subproof i (x : ext_num_def i)
+    (r := itv_real1_subdef fine_itv_subdef i) :
+  num_spec r (fine x%:num).
+Proof.
+rewrite {}/r; case: i x => [//| [l u] [x /=/and3P[xr /= lx xu]]].
+apply/and3P; split; rewrite -?real_fine//.
+- case: x lx {xu xr} => [x||]/=; [|by case: l => [? []|]..].
+  by case: l => [[] [l |//] |//] /[!bnd_simp] => [|/ltW]/=; rewrite lee_fin;
+     apply: le_trans.
+- case: x xu {lx xr} => [x||]/=; [|by case: u => [? [[]|] |]..].
+  by case: u => [bu [[|//] | u] |//]; case: bu => /[!bnd_simp] [/ltW|]/=;
+     rewrite lee_fin// => xu; apply: le_trans xu _; rewrite lerz0.
+Qed.
 
-Canonical ninfty_snum := Signed.mk (ninfty_snum_subproof).
+Canonical fine_inum i (x : ext_num_def i) := Itv.mk (fine_inum_subproof x).
 
-Lemma EFin_snum_subproof nz cond (x : {num R & nz & cond}) :
-  Signed.spec 0 nz cond x%:num%:E.
+Lemma ext_num_sem_y l u :
+  ext_num_sem (Interval l u) +oo = ((l != +oo%O) && (u == +oo%O)).
 Proof.
-apply/andP; split.
-  case: cond nz x => [[[]|]|] [] x //=;
-    do ?[by case: (bottom x)|by rewrite eqe eq0F].
-case: cond nz x => [[[]|]|] [] x //=;
-  do ?[by case: (bottom x)|by rewrite ?lee_fin ?(eq0, ge0, le0) ?[_ || _]cmp0].
+apply/and3P/andP => [[_ ly uy] | [ly uy]]; split.
+- by case: l ly => -[].
+- by case: u uy => -[].
+- exact: cmp0y.
+- case: l ly => [|[]//].
+  by case=> l _ /=; rewrite bnd_simp ?real_leey ?real_ltry /= realz.
+- by case: u uy => -[].
 Qed.
 
-Canonical EFin_snum nz cond (x : {num R & nz & cond}) :=
-  Signed.mk (EFin_snum_subproof x).
+Lemma ext_num_sem_Ny l u :
+  ext_num_sem (Interval l u) -oo = ((l == -oo%O) && (u != -oo%O)).
+Proof.
+apply/and3P/andP => [[_ ly uy] | [ly uy]]; split.
+- by case: l ly => -[].
+- by case: u uy => -[].
+- exact: real0.
+- by case: l ly => -[].
+- case: u uy => [|[]//].
+  by case=> u _ /=; rewrite bnd_simp ?real_leNye ?real_ltNyr /= realz.
+Qed.
 
-Lemma fine_snum_subproof (xnz : KnownSign.nullity) (xr : KnownSign.reality)
-    (x : {compare (0 : \bar R) & xnz & xr}) :
-  Signed.spec 0%R ?=0 xr (fine x%:num).
+Lemma oppe_itv_boundr_subproof (x : \bar R) b :
+  (BRight (- x) <= ext_num_itv_bound (opp_itv_bound_subdef b))%O
+  = (ext_num_itv_bound b <= BLeft x)%O.
 Proof.
-case: xr x => [[[]|]|]//= [x /andP[_]]/=.
-- by move=> /eqP ->.
-- by case: x.
-- by case: x.
-- by move=> /orP[]; case: x => [x||]//=; rewrite lee_fin => ->; rewrite ?orbT.
+by case: b => [[] b | []//]; rewrite /= !bnd_simp mulrNz EFinN ?leeN2 // lteN2.
 Qed.
 
-Canonical fine_snum (xnz : KnownSign.nullity) (xr : KnownSign.reality)
-    (x : {compare (0 : \bar R) & xnz & xr}) :=
-  Signed.mk (fine_snum_subproof x).
+Lemma oppe_itv_boundl_subproof (x : \bar R) b :
+  (ext_num_itv_bound (opp_itv_bound_subdef b) <= BLeft (- x))%O
+  = (BRight x <= ext_num_itv_bound b)%O.
+Proof.
+by case: b => [[] b | []//]; rewrite /= !bnd_simp mulrNz EFinN ?leeN2 // lteN2.
+Qed.
 
-Lemma oppe_snum_subproof (xnz : KnownSign.nullity) (xr : KnownSign.reality)
-    (x : {compare (0 : \bar R) & xnz & xr}) (r := opp_reality_subdef xnz xr) :
-  Signed.spec 0 xnz r (- x%:num).
+Lemma oppe_inum_subproof i (x : ext_num_def i)
+    (r := itv_real1_subdef opp_itv_subdef i) :
+  ext_num_spec r (- x%:inum).
 Proof.
-rewrite {}/r; case: xr xnz x => [[[]|]|] [] x //=;
-  do ?[by case: (bottom x)
-      |by rewrite ?eqe_oppLR ?oppe0 1?eq0//;
-          rewrite ?oppe_le0 ?oppe_ge0 ?(eq0, eq0F, ge0, le0)//;
-          rewrite orbC [_ || _]cmp0].
+rewrite {}/r; case: x => -[x||]/=;
+  [|by case: i => [//| [l u]]; rewrite /= ext_num_sem_y ext_num_sem_Ny;
+       case: l u => [[] ?|[]] [[] ?|[]]..].
+rewrite !ext_num_num_spec_subproof => Px.
+by rewrite -[x]/(Itv.mk Px)%:inum opp_inum_subproof.
 Qed.
 
-Canonical oppe_snum (xnz : KnownSign.nullity) (xr : KnownSign.reality)
-    (x : {compare (0 : \bar R) & xnz & xr}) :=
-  Signed.mk (oppe_snum_subproof x).
+Canonical oppe_inum i (x : ext_num_def i) := Itv.mk (oppe_inum_subproof x).
 
-Lemma adde_snum_subproof (xnz ynz : KnownSign.nullity)
-    (xr yr : KnownSign.reality)
-    (x : {compare (0 : \bar R) & xnz & xr})
-    (y : {compare (0 : \bar R) & ynz & yr})
-    (rnz := add_nonzero_subdef xnz ynz xr yr)
-    (rrl := add_reality_subdef xnz ynz xr yr) :
-  Signed.spec 0 rnz rrl (adde x%:num y%:num).
+Lemma adde_inum_subproof xi yi (x : ext_num_def xi) (y : ext_num_def yi)
+    (r := itv_real2_subdef add_itv_subdef xi yi) :
+  ext_num_spec r (adde x%:inum y%:inum).
 Proof.
-rewrite {}/rnz {}/rrl; apply/andP; split.
-  move: xr yr xnz ynz x y => [[[]|]|] [[[]|]|] [] []//= x y;
-  by rewrite 1?adde_ss_eq0 ?(eq0F, ge0, le0, andbF, orbT).
-move: xr yr xnz ynz x y => [[[]|]|] [[[]|]|] [] []//= x y;
-  do ?[by case: (bottom x)|by case: (bottom y)
-      |by rewrite adde_ge0|by rewrite adde_le0
-      |exact: realDe|by rewrite 2!eq0 /adde/= addr0].
+rewrite {}/r; case: x y => -[x||] + [[y||]]/=;
+  [|by case: xi yi => [//| [xl xu]] [//| [yl yu]];
+       rewrite /adde/= ?ext_num_sem_y ?ext_num_sem_Ny;
+       case: xl xu yl yu => [[] ?|[]] [[] ?|[]] [[] ?|[]] [[] ?|[]]..].
+rewrite !ext_num_num_spec_subproof => Px Py.
+by rewrite -[x]/(Itv.mk Px)%:inum -[y]/(Itv.mk Py)%:inum add_inum_subproof.
 Qed.
 
-Canonical adde_snum (xnz ynz : KnownSign.nullity)
-    (xr yr : KnownSign.reality)
-    (x : {compare (0 : \bar R) & xnz & xr})
-    (y : {compare (0 : \bar R) & ynz & yr}) :=
-  Signed.mk (adde_snum_subproof x y).
+Canonical adde_inum xi yi (x : ext_num_def xi) (y : ext_num_def yi) :=
+  Itv.mk (adde_inum_subproof x y).
 
 Import DualAddTheory.
 
-Lemma dEFin_snum_subproof nz cond (x : {num R & nz & cond}) :
-  Signed.spec 0 nz cond (dEFin x%:num).
-Proof. exact: EFin_snum_subproof. Qed.
-
-Canonical dEFin_snum nz cond (x : {num R & nz & cond}) :=
-  Signed.mk (dEFin_snum_subproof x).
-
-Lemma dadde_snum_subproof (xnz ynz : KnownSign.nullity)
-    (xr yr : KnownSign.reality)
-    (x : {compare (0 : \bar R) & xnz & xr})
-    (y : {compare (0 : \bar R) & ynz & yr})
-    (rnz := add_nonzero_subdef xnz ynz xr yr)
-    (rrl := add_reality_subdef xnz ynz xr yr) :
-  Signed.spec 0 rnz rrl (dual_adde x%:num y%:num)%dE.
-Proof.
-rewrite {}/rnz {}/rrl; apply/andP; split.
-  move: xr yr xnz ynz x y => [[[]|]|] [[[]|]|] [] []//= x y;
-  by rewrite 1?dadde_ss_eq0 ?(eq0F, ge0, le0, andbF, orbT).
-move: xr yr xnz ynz x y => [[[]|]|] [[[]|]|] [] []//= x y;
-  do ?[by case: (bottom x)|by case: (bottom y)
-      |by rewrite dadde_ge0|by rewrite dadde_le0
-      |exact: realDed|by rewrite 2!eq0 /dual_adde/= addr0].
-Qed.
-
-Canonical dadde_snum (xnz ynz : KnownSign.nullity)
-    (xr yr : KnownSign.reality)
-    (x : {compare (0 : \bar R) & xnz & xr})
-    (y : {compare (0 : \bar R) & ynz & yr}) :=
-  Signed.mk (dadde_snum_subproof x y).
-
-Lemma mule_snum_subproof (xnz ynz : KnownSign.nullity)
-    (xr yr : KnownSign.reality)
-    (x : {compare (0 : \bar R) & xnz & xr})
-    (y : {compare (0 : \bar R) & ynz & yr})
-    (rnz := mul_nonzero_subdef xnz ynz xr yr)
-    (rrl := mul_reality_subdef xnz ynz xr yr) :
-  Signed.spec 0 rnz rrl (x%:num * y%:num).
-Proof.
-rewrite {}/rnz {}/rrl; apply/andP; split.
-  by move: xr yr xnz ynz x y => [[[]|]|] [[[]|]|] [] []// x y;
-     rewrite mule_neq0.
-by move: xr yr xnz ynz x y => [[[]|]|] [[[]|]|] [] []/= x y //;
-  do ?[by case: (bottom x)|by case: (bottom y)
-      |by rewrite mule_ge0|by rewrite mule_le0_ge0
-      |by rewrite mule_ge0_le0|by rewrite mule_le0|exact: realMe
-      |by rewrite eq0 ?mule0// mul0e].
-Qed.
-
-Canonical mule_snum (xnz ynz : KnownSign.nullity) (xr yr : KnownSign.reality)
-    (x : {compare (0 : \bar R) & xnz & xr})
-    (y : {compare (0 : \bar R) & ynz & yr}) :=
-  Signed.mk (mule_snum_subproof x y).
-
-Definition abse_reality_subdef (xnz : KnownSign.nullity)
-    (xr : KnownSign.reality) := (if xr is =0 then =0 else >=0)%snum_sign.
-Arguments abse_reality_subdef /.
-
-Lemma abse_snum_subproof (xnz : KnownSign.nullity) (xr : KnownSign.reality)
-    (x : {compare (0 : \bar R) & xnz & xr}) (r := abse_reality_subdef xnz xr) :
-  Signed.spec 0 xnz r `|x%:num|.
-Proof.
-rewrite {}/r; case: xr xnz x => [[[]|]|] [] x //=;
-  do ?[by case: (bottom x)|by rewrite eq0 abse0
-      |by rewrite abse_ge0// andbT gee0_abs
-      |by rewrite abse_ge0// andbT lee0_abs
-      |by rewrite abse_ge0// andbT abse_eq0].
-Qed.
-
-Canonical abse_snum (xnz : KnownSign.nullity) (xr : KnownSign.reality)
-    (x : {compare (0 : \bar R) & xnz & xr}) :=
-  Signed.mk (abse_snum_subproof x).
-
-End SignedNumDomainStability.
+Lemma dEFin_inum_subproof i (x : num_def R i) : ext_num_spec i (dEFin x%:num).
+Proof.
+case: i x => [//| [l u] [x /=/and3P[xr /= lx xu]]].
+by apply/and3P; split=> [//||]; [case: l lx | case: u xu].
+Qed.
+
+Canonical dEFin_inum i (x : num_def R i) := Itv.mk (dEFin_inum_subproof x).
+
+Lemma dadde_inum_subproof xi yi (x : ext_num_def xi) (y : ext_num_def yi)
+    (r := itv_real2_subdef add_itv_subdef xi yi) :
+  ext_num_spec r (dual_adde x%:inum y%:inum).
+Proof.
+rewrite {}/r; case: x y => -[x||] + [[y||]]/=;
+  [|by case: xi yi => [//| [xl xu]] [//| [yl yu]];
+       rewrite /dual_adde/= ?ext_num_sem_y ?ext_num_sem_Ny;
+       case: xl xu yl yu => [[] ?|[]] [[] ?|[]] [[] ?|[]] [[] ?|[]]..].
+rewrite !ext_num_num_spec_subproof => Px Py.
+by rewrite -[x]/(Itv.mk Px)%:inum -[y]/(Itv.mk Py)%:inum add_inum_subproof.
+Qed.
+
+Canonical dadde_inum xi yi (x : ext_num_def xi) (y : ext_num_def yi) :=
+  Itv.mk (dadde_inum_subproof x y).
+
+Variant ext_interval_sign_spec (l u : itv_bound int) (x : \bar R) :
+      signi -> Set :=
+  | ISignEqZero : l = BLeft 0%Z -> u = BRight 0%Z -> x = 0 ->
+                  ext_interval_sign_spec l u x (Known EqZero)
+  | ISignNonNeg : (BLeft 0%:Z <= l)%O -> (BRight 0%:Z < u)%O -> 0 <= x ->
+                  ext_interval_sign_spec l u x (Known NonNeg)
+  | ISignNonPos : (l < BLeft 0%:Z)%O -> (u <= BRight 0%:Z)%O -> x <= 0 ->
+                  ext_interval_sign_spec l u x (Known NonPos)
+  | ISignBoth : (l < BLeft 0%:Z)%O -> (BRight 0%:Z < u)%O ->
+                (0 >=< x)%O -> ext_interval_sign_spec l u x Unknown.
+
+Lemma ext_interval_signP (l u : itv_bound int) (x : \bar R) :
+    (ext_num_itv_bound l <= BLeft x)%O -> (BRight x <= ext_num_itv_bound u)%O ->
+    (0 >=< x)%O ->
+  ext_interval_sign_spec l u x (interval_sign (Interval l u)).
+Proof.
+case: x => [x||] xl xu xs.
+- case: (@interval_signP R l u x _ _ xs).
+  + by case: l xl => -[].
+  + by case: u xu => -[].
+  + by move=> l0 u0 x0; apply: ISignEqZero => //; rewrite x0.
+  + by move=> l0 u0 x0; apply: ISignNonNeg.
+  + by move=> l0 u0 x0; apply: ISignNonPos.
+  + by move=> l0 u0 x0; apply: ISignBoth.
+- have uy : u = +oo%O by case: u xu => -[].
+  have u0 : (BRight 0%:Z < u)%O by rewrite uy.
+  case: (leP (BLeft 0%Z) l) => l0.
+  + suff -> : interval_sign (Interval l u) = Known NonNeg.
+      by apply: ISignNonNeg => //; apply: le0y.
+    rewrite /=/itv_bound_signl /itv_bound_signr uy/=.
+    by case: eqP => [//| /eqP lneq0]; case: ltgtP l0 lneq0.
+  + suff -> : interval_sign (Interval l u) = Unknown by exact: ISignBoth.
+    rewrite /=/itv_bound_signl /itv_bound_signr uy/=.
+    by case: eqP l0 => [->//| /eqP leq0] /ltW->.
+- have ly : l = -oo%O by case: l xl => -[].
+  have l0 : (l < BLeft 0%:Z)%O by rewrite ly.
+  case: (leP u (BRight 0%Z)) => u0.
+  + suff -> : interval_sign (Interval l u) = Known NonPos by exact: ISignNonPos.
+    rewrite /=/itv_bound_signl /itv_bound_signr ly/=.
+    by case: eqP => [//| /eqP uneq0]; case: ltgtP u0 uneq0.
+  + suff -> : interval_sign (Interval l u) = Unknown by exact: ISignBoth.
+    rewrite /=/itv_bound_signl /itv_bound_signr ly/=.
+    by case: eqP u0 => [->//| /eqP ueq0]; rewrite ltNge => /negbTE->.
+Qed.
+
+Lemma ext_mul_itv_boundl_subproof b1 b2 (x1 x2 : \bar R) :
+  (BLeft 0%:Z <= b1 -> BLeft 0%:Z <= b2 ->
+   ext_num_itv_bound b1 <= BLeft x1 ->
+   ext_num_itv_bound b2 <= BLeft x2 ->
+   ext_num_itv_bound (mul_itv_boundl_subdef b1 b2) <= BLeft (x1 * x2))%O.
+Proof.
+move=> b10 b20 b1x1 b2x2.
+have x10 : 0 <= x1.
+  by case: x1 b1x1 (le_trans (eqbRL (ext_le_map_itv_bound _ _) b10) b1x1).
+have x20 : 0 <= x2.
+  by case: x2 b2x2 (le_trans (eqbRL (ext_le_map_itv_bound _ _) b20) b2x2).
+have x1r : (0 >=< x1)%O by rewrite real_fine; exact/ger0_real/fine_ge0.
+have x2r : (0 >=< x2)%O by rewrite real_fine; exact/ger0_real/fine_ge0.
+have ley b1' b2' :
+    (Itv.map_itv_bound EFin (num_itv_bound R (mul_itv_boundl_subdef b1' b2'))
+     <= BLeft +oo%E)%O.
+  by case: b1' b2' => [[] [[| ?] | ?] | []] [[] [[| ?] | ?] | []]//=;
+     rewrite bnd_simp ?real_leey ?real_ltry/= ?realz.
+case: x1 x2 x10 x20 x1r x2r b1x1 b2x2 => [x1||] [x2||] //= x10 x20 x1r x2r.
+- rewrite !(map_itv_bound_comp, EFin_BLeft_le_map_itv_bound)/=.
+  exact: mul_itv_boundl_subproof.
+- rewrite !(map_itv_bound_comp EFin intr) real_mulry//= => b1x1 _.
+  case: (comparable_ltgtP x1r) x10 => [x10 |//| [x10]] _.
+    by rewrite gtr0_sg ?mul1e ?bnd_simp.
+  rewrite -x10 sgr0 mul0e/= EFin_BLeft_le_map_itv_bound.
+  suff -> : b1 = BLeft 0%Z by case: b2 {b20}.
+  apply/le_anti; rewrite b10 andbT.
+  move: b1x1; rewrite EFin_BLeft_le_map_itv_bound.
+  by rewrite -x10 -(mulr0z 1) intr_BLeft_le_map_itv_bound.
+- rewrite !(map_itv_bound_comp EFin intr) real_mulyr//= => _ b2x2.
+  case: (comparable_ltgtP x2r) x20 => [x20 |//| [x20]] _.
+    by rewrite gtr0_sg ?mul1e ?bnd_simp.
+  rewrite -x20 sgr0 mul0e/= EFin_BLeft_le_map_itv_bound.
+  suff -> : b2 = BLeft 0%Z by case: b1 {b10} => [[] [] []|].
+  apply/le_anti; rewrite b20 andbT.
+  move: b2x2; rewrite EFin_BLeft_le_map_itv_bound.
+  by rewrite -x20 -(mulr0z 1) intr_BLeft_le_map_itv_bound.
+- by rewrite mulyy/= 3!map_itv_bound_comp.
+Qed.
+
+Lemma ext_mul_itv_boundr_subproof b1 b2 (x1 x2 : \bar R) :
+  (0 <= x1 -> 0 <= x2 ->
+   BRight x1 <= ext_num_itv_bound b1 ->
+   BRight x2 <= ext_num_itv_bound b2 ->
+   BRight (x1 * x2) <= ext_num_itv_bound (mul_itv_boundr_subdef b1 b2))%O.
+Proof.
+move=> x10 x20 b1x1 b2x2.
+have x1r : (0 >=< x1)%O by rewrite real_fine; exact/ger0_real/fine_ge0.
+have x2r : (0 >=< x2)%O by rewrite real_fine; exact/ger0_real/fine_ge0.
+case: x1 x2 x10 x20 x1r x2r b1x1 b2x2 => [x1||] [x2||] //= x10 x20 x1r x2r.
+- rewrite !(map_itv_bound_comp, BRight_EFin_le_map_itv_bound)/=.
+  exact: mul_itv_boundr_subproof.
+- rewrite real_mulry// => b1x1 b2x2.
+  have -> : b2 = +oo%O by case: b2 b2x2 => -[].
+  rewrite mul_itv_boundrC_subproof/= map_itv_bound_comp.
+  case: (comparable_ltgtP x1r) x10 => [x10 |//| [x10]] _.
+  + rewrite gtr0_sg ?mul1e ?bnd_simp//.
+    suff: (BRight 0%Z < b1)%O by case: b1 b1x1 => [[] [] [] |].
+    move: b1x1; rewrite map_itv_bound_comp BRight_EFin_le_map_itv_bound.
+    case: b1 => [[] b1 |//]; rewrite !bnd_simp -(@ltr0z R).
+    * exact/le_lt_trans/ltW.
+    * exact/lt_le_trans.
+  + rewrite -x10 sgr0 mul0e/= BRight_EFin_le_map_itv_bound.
+    suff: (BRight 0%Z <= b1)%O by case: b1 b1x1 => [[] [] [] |].
+    move: b1x1; rewrite map_itv_bound_comp BRight_EFin_le_map_itv_bound.
+    by rewrite -x10 -(@mulr0z R 1) BRight_intr_le_map_itv_bound.
+- rewrite real_mulyr// => b1x1 b2x2.
+  have -> : b1 = +oo%O by case: b1 b1x1 => -[].
+  rewrite /= map_itv_bound_comp.
+  case: (comparable_ltgtP x2r) x20 => [x20 |//| [x20]] _.
+  + rewrite gtr0_sg ?mul1e ?bnd_simp//.
+    suff: (BRight 0%Z < b2)%O by case: b2 b2x2 => [[] [] [] |].
+    move: b2x2; rewrite map_itv_bound_comp BRight_EFin_le_map_itv_bound.
+    case: b2 => [[] b2 |//]; rewrite !bnd_simp -(@ltr0z R).
+    * exact/le_lt_trans/ltW.
+    * exact/lt_le_trans.
+  + rewrite -x20 sgr0 mul0e/= BRight_EFin_le_map_itv_bound.
+    suff: (BRight 0%Z <= b2)%O by case: b2 b2x2 => [[] [] [] |].
+    move: b2x2; rewrite map_itv_bound_comp BRight_EFin_le_map_itv_bound.
+    by rewrite -x20 -(@mulr0z R 1) BRight_intr_le_map_itv_bound.
+- rewrite mulyy/= => b1x1 b2x2.
+  have -> : b1 = +oo%O by case: b1 b1x1 => -[].
+  by have -> : b2 = +oo%O by case: b2 b2x2 => -[].
+Qed.
+
+Lemma ext_mul_itv_boundr'_subproof b1 b2 (x1 x2 : \bar R) :
+  (0 <= x1 -> (0 >=< x2)%O -> BRight 0%Z <= b2 ->
+   BRight x1 <= ext_num_itv_bound b1 ->
+   BRight x2 <= ext_num_itv_bound b2 ->
+   BRight (x1 * x2) <= ext_num_itv_bound (mul_itv_boundr_subdef b1 b2))%O.
+Proof.
+move=> x1ge0 x2r b2ge0 lex1b1 lex2b2.
+have /orP[x2ge0 | x2le0] : (0 <= x2) || (x2 <= 0).
+- by case: x2 x2r {lex2b2} => [x2 /=|_|_]; rewrite ?lee_fin ?le0y ?leNy0.
+- exact: ext_mul_itv_boundr_subproof.
+have lem0 : (BRight (x1 * x2) <= BRight 0%R)%O.
+  by have:= mule_ge0_le0 x1ge0 x2le0; case: mule.
+apply: le_trans lem0 _.
+rewrite map_itv_bound_comp BRight_EFin_le_map_itv_bound/=.
+rewrite -(@mulr0z R 1) BRight_intr_le_map_itv_bound.
+apply: mul_itv_boundr_BRight_subproof => //.
+case: x1 x1ge0 lex1b1 => [x1||//]/= x1ge0; last by case: b1 => -[].
+rewrite map_itv_bound_comp BRight_EFin_le_map_itv_bound.
+rewrite -(@BRight_intr_le_map_itv_bound R)/=.
+by apply: le_trans; rewrite bnd_simp -lee_fin.
+Qed.
+
+Lemma comparable_ext_num_itv_bound_subproof (x y : itv_bound int) :
+  (ext_num_itv_bound x >=< ext_num_itv_bound y)%O.
+Proof.
+apply/orP; rewrite !(map_itv_bound_comp EFin intr)/= !EFin_le_map_itv_bound.
+exact/orP/comparable_num_itv_bound_subproof.
+Qed.
+
+Lemma ext_map_itv_bound_min (x y : itv_bound int) :
+  ext_num_itv_bound (Order.min x y)
+  = Order.min (ext_num_itv_bound x) (ext_num_itv_bound y).
+Proof.
+have [lexy | ltyx] := leP x y; [by rewrite !minEle ext_le_map_itv_bound lexy|].
+rewrite minElt -if_neg -comparable_leNgt ?ext_le_map_itv_bound ?ltW//.
+exact: comparable_ext_num_itv_bound_subproof.
+Qed.
+
+Lemma ext_map_itv_bound_max (x y : itv_bound int) :
+  ext_num_itv_bound (Order.max x y)
+  = Order.max (ext_num_itv_bound x) (ext_num_itv_bound y).
+Proof.
+have [lexy | ltyx] := leP x y; [by rewrite !maxEle ext_le_map_itv_bound lexy|].
+rewrite maxElt -if_neg -comparable_leNgt ?ext_le_map_itv_bound ?ltW//.
+exact: comparable_ext_num_itv_bound_subproof.
+Qed.
+
+Lemma mule_inum_subproof xi yi (x : ext_num_def xi) (y : ext_num_def yi)
+    (r := itv_real2_subdef mul_itv_subdef xi yi) :
+  ext_num_spec r (x%:inum * y%:inum).
+Proof.
+rewrite {}/r; case: xi yi x y => [//| [xl xu]] [//| [yl yu]].
+case=> [x /=/and3P[xr /= xlx xxu]] [y /=/and3P[yr /= yly yyu]].
+rewrite -/(interval_sign (Interval xl xu)) -/(interval_sign (Interval yl yu)).
+have ns000 : ext_num_sem `[0%Z, 0%Z] 0 by apply/and3P; rewrite ?comparablexx.
+have xyr : (0 >=< (x * y)%E)%O by exact: realMe.
+case: (ext_interval_signP xlx xxu xr) => xlb xub xs.
+- by rewrite xs mul0e; case: (ext_interval_signP yly yyu yr).
+- case: (ext_interval_signP yly yyu yr) => ylb yub ys.
+  + by rewrite ys mule0.
+  + apply/and3P; split=> //=.
+    * exact: ext_mul_itv_boundl_subproof.
+    * exact: ext_mul_itv_boundr_subproof.
+  + apply/and3P; split=> //=; rewrite -[x * y]oppeK -real_muleN//.
+    * rewrite oppe_itv_boundl_subproof.
+      by rewrite ext_mul_itv_boundr_subproof ?oppe_ge0 ?oppe_itv_boundr_subproof.
+    * rewrite oppe_itv_boundr_subproof.
+      rewrite ext_mul_itv_boundl_subproof ?oppe_itv_boundl_subproof//.
+      by rewrite opp_itv_ge0_subproof.
+  + apply/and3P; split=> //=.
+    * rewrite  -[x * y]oppeK -real_muleN// oppe_itv_boundl_subproof.
+      rewrite ext_mul_itv_boundr'_subproof -?real_fine ?oppe_cmp0
+              ?oppe_itv_boundr_subproof//.
+      by rewrite opp_itv_gt0_subproof ltW.
+    * by rewrite ext_mul_itv_boundr'_subproof// ltW.
+- case: (ext_interval_signP yly yyu yr) => ylb yub ys.
+  + by rewrite ys mule0.
+  + apply/and3P; split=> //=; rewrite -[x * y]oppeK -real_mulNe//.
+    * rewrite oppe_itv_boundl_subproof.
+      by rewrite ext_mul_itv_boundr_subproof ?oppe_ge0 ?oppe_itv_boundr_subproof.
+    * rewrite oppe_itv_boundr_subproof.
+      rewrite ext_mul_itv_boundl_subproof ?oppe_itv_boundl_subproof//.
+      by rewrite opp_itv_ge0_subproof.
+  + apply/and3P; split=> //=; rewrite -real_muleNN//.
+    * by rewrite ext_mul_itv_boundl_subproof
+        ?opp_itv_ge0_subproof ?oppe_itv_boundl_subproof.
+    * by rewrite ext_mul_itv_boundr_subproof ?oppe_ge0 ?oppe_itv_boundr_subproof.
+  + apply/and3P; split=> //=; rewrite -[x * y]oppeK.
+    * rewrite -real_mulNe// oppe_itv_boundl_subproof.
+      rewrite ext_mul_itv_boundr'_subproof ?oppe_ge0 ?oppe_itv_boundr_subproof//.
+      exact: ltW.
+    * rewrite oppeK -real_muleNN//.
+      by rewrite ext_mul_itv_boundr'_subproof ?oppe_itv_boundr_subproof
+                 ?oppe_ge0 ?oppe_cmp0 ?opp_itv_gt0_subproof// ltW.
+- case: (ext_interval_signP yly yyu yr) => ylb yub ys.
+  + by rewrite ys mule0.
+  + apply/and3P; split=> //=; rewrite muleC mul_itv_boundrC_subproof.
+    * rewrite -[y * x]oppeK -real_muleN// oppe_itv_boundl_subproof.
+      rewrite ext_mul_itv_boundr'_subproof ?oppe_ge0 ?oppe_cmp0
+              ?oppe_itv_boundr_subproof//.
+      by rewrite opp_itv_gt0_subproof ltW.
+    * by rewrite ext_mul_itv_boundr'_subproof// ltW.
+  + apply/and3P; split=> //=; rewrite muleC mul_itv_boundrC_subproof.
+    * rewrite -[y * x]oppeK -real_mulNe// oppe_itv_boundl_subproof.
+      rewrite ext_mul_itv_boundr'_subproof ?oppe_ge0 ?oppe_itv_boundr_subproof//.
+      exact: ltW.
+    * rewrite -real_muleNN// ext_mul_itv_boundr'_subproof ?oppe_ge0
+              ?oppe_cmp0 ?oppe_itv_boundr_subproof//.
+      by rewrite opp_itv_gt0_subproof ltW.
+apply/and3P; rewrite xyr/= ext_map_itv_bound_min ext_map_itv_bound_max.
+rewrite (comparable_ge_min _ (comparable_ext_num_itv_bound_subproof _ _)).
+rewrite (comparable_le_max _ (comparable_ext_num_itv_bound_subproof _ _)).
+have [x0 | /ltW x0] : 0 <= x \/ x < 0; [|split=> //..].
+  case: x xr {xlx xxu xyr xs} => [x||] /= xr.
+  - by case: (comparable_leP xr) => x0; [left | right].
+  - by left; rewrite le0y.
+  - by right; rewrite ltNy0.
+- apply/orP; right; rewrite -[x * y]oppeK -real_muleN// oppe_itv_boundl_subproof.
+  rewrite ext_mul_itv_boundr'_subproof ?oppe_cmp0 ?oppe_itv_boundr_subproof//.
+  by rewrite opp_itv_gt0_subproof ltW.
+- by apply/orP; right; rewrite ext_mul_itv_boundr'_subproof// ltW.
+- apply/orP; left; rewrite -[x * y]oppeK -real_mulNe// oppe_itv_boundl_subproof.
+  rewrite ext_mul_itv_boundr'_subproof ?oppe_ge0 ?oppe_itv_boundr_subproof//.
+  exact: ltW.
+- apply/orP; left; rewrite -real_muleNN//.
+  rewrite ext_mul_itv_boundr'_subproof ?oppe_ge0 ?oppe_cmp0
+          ?oppe_itv_boundr_subproof//.
+  by rewrite opp_itv_gt0_subproof ltW.
+Qed.
+
+Canonical mule_inum xi yi (x : ext_num_def xi) (y : ext_num_def yi) :=
+  Itv.mk (mule_inum_subproof x y).
+
+Definition abse_itv_subdef (i : Itv.t) : Itv.t :=
+  match i with
+  | Itv.Top => Itv.Real `[0%Z, +oo[
+  | Itv.Real (Interval l u) =>
+    match l with
+    | BRight (Posz _) | BLeft (Posz (S _)) => Itv.Real `]0%Z, +oo[
+    | _ => Itv.Real `[0%Z, +oo[
+    end
+  end.
+Arguments abse_itv_subdef /.
+
+Lemma abse_inum_subproof i (x : ext_num_def i)
+    (r := abse_itv_subdef i) :
+  ext_num_spec r `|x%:inum|.
+Proof.
+have: ext_num_sem `[0%Z, +oo[ `|x%:inum|.
+  apply/and3P; split; rewrite ?bnd_simp ?abse_ge0//.
+  by case: x%:inum => [x'||]; rewrite ?cmp0y// le_comparable ?abse_ge0.
+have: 0 < x%:inum -> ext_num_sem `]0%Z, +oo[ `|x%:inum|.
+  move=> xgt0; apply/and3P; split; rewrite ?bnd_simp//.
+  - by case: x%:num => [x'||]; rewrite ?cmp0y// le_comparable ?abse_ge0.
+  - case: x%:inum xgt0 => [x'|//|//]/=.
+    by rewrite !lte_fin normr_gt0; apply: lt0r_neq0.
+rewrite {}/r; case: i x => [//| [[[] [[//| l] | //] | //] u]] [x /=] + + _;
+    move/and3P => [xr /= /[!bnd_simp]lx _]; apply.
+- by apply: lt_le_trans lx; rewrite lte_fin ltr0z.
+- by apply: le_lt_trans lx; rewrite lee_fin ler0z.
+- by apply: lt_trans lx; rewrite lte_fin ltr0z.
+Qed.
+
+Canonical abse_inum i (x : ext_num_def i) := Itv.mk (abse_inum_subproof x).
+
+Lemma ext_min_itv_boundl_subproof x1 x2 b1 b2 :
+  (ext_num_itv_bound b1 <= BLeft x1)%O ->
+  (ext_num_itv_bound b2 <= BLeft x2)%O ->
+  (ext_num_itv_bound (Order.min b1 b2) <= BLeft (Order.min x1 x2))%O.
+Proof.
+case: (leP b1 b2) => [b1_le_b2 | /ltW b2_le_b1].
+- have sb1_le_sb2 := eqbRL (ext_le_map_itv_bound _ _) b1_le_b2.
+  by rewrite minElt; case: (x1 < x2)%O => [//|_]; apply: le_trans.
+- have sb2_le_sb1 := eqbRL (ext_le_map_itv_bound _ _) b2_le_b1.
+  by rewrite minElt; case: (x1 < x2)%O => [+ _|//]; apply: le_trans.
+Qed.
+
+Lemma ext_min_itv_boundr_subproof x1 x2 b1 b2 : (x1 >=< x2)%O ->
+  (BRight x1 <= ext_num_itv_bound b1)%O ->
+  (BRight x2 <= ext_num_itv_bound b2)%O ->
+  (BRight (Order.min x1 x2) <= ext_num_itv_bound (Order.min b1 b2))%O.
+Proof.
+move=> x1_cmp_x2; case: (leP b1 b2) => [b1_le_b2 | /ltW b2_le_b1].
+- have sb1_le_sb2 := eqbRL (ext_le_map_itv_bound _ _) b1_le_b2.
+  by case: (comparable_leP x1_cmp_x2) => [//| /ltW ? + _]; apply: le_trans.
+- have sb2_le_sb1 := eqbRL (ext_le_map_itv_bound _ _) b2_le_b1.
+  by case: (comparable_leP x1_cmp_x2) => [? _ |//]; apply: le_trans.
+Qed.
+
+Lemma ext_min_inum_subproof (xi yi : Itv.t)
+    (x : ext_num_def xi) (y : ext_num_def yi)
+    (r := itv_real2_subdef min_itv_subdef xi yi) :
+  ext_num_spec r (Order.min x%:inum y%:inum).
+Proof.
+apply: itv_real2_subproof (Itv.P x) (Itv.P y).
+case: x y => [x /= _] [y /= _] => {xi yi r} -[lx ux] [ly uy]/=.
+move=> /andP[xr /=/andP[lxx xux]] /andP[yr /=/andP[lyy yuy]].
+apply/and3P; split.
+- case: x y xr yr {lxx xux lyy yuy} => [x||] [y||]//=.
+  + by move=> ? ?; apply: comparable_minr.
+  + by move=> ? ?; rewrite real_miney.
+  + by move=> ? ?; rewrite real_minNye.
+- exact: ext_min_itv_boundl_subproof.
+- by apply: ext_min_itv_boundr_subproof => //; apply: ereal_comparable.
+Qed.
+
+Lemma ext_max_itv_boundl_subproof x1 x2 b1 b2 : (x1 >=< x2)%O ->
+  (ext_num_itv_bound b1 <= BLeft x1)%O ->
+  (ext_num_itv_bound b2 <= BLeft x2)%O ->
+  (ext_num_itv_bound (Order.max b1 b2) <= BLeft (Order.max x1 x2))%O.
+Proof.
+move=> x1_cmp_x2.
+case: (leP b1 b2) => [b1_le_b2 | /ltW b2_le_b1].
+- case: (comparable_leP x1_cmp_x2) => [//| /ltW ? _ sb2_x2].
+  exact: le_trans sb2_x2 _.
+- case: (comparable_leP x1_cmp_x2) => [? sb1_x1 _ |//].
+  exact: le_trans sb1_x1 _.
+Qed.
+
+Lemma ext_max_itv_boundr_subproof x1 x2 b1 b2 :
+  (BRight x1 <= ext_num_itv_bound b1)%O ->
+  (BRight x2 <= ext_num_itv_bound b2)%O ->
+  (BRight (Order.max x1 x2) <= ext_num_itv_bound (Order.max b1 b2))%O.
+Proof.
+case: (leP b1 b2) => [b1_le_b2 | /ltW b2_le_b1].
+- have sb1_le_sb2 := eqbRL (ext_le_map_itv_bound _ _) b1_le_b2.
+  by rewrite maxElt; case: ifP => [//|_ ? _]; apply: le_trans sb1_le_sb2.
+- have sb2_le_sb1 := eqbRL (ext_le_map_itv_bound _ _) b2_le_b1.
+  by rewrite maxElt; case: ifP => [_ _ ?|//]; apply: le_trans sb2_le_sb1.
+Qed.
+
+Lemma ext_max_inum_subproof (xi yi : Itv.t)
+    (x : ext_num_def xi) (y : ext_num_def yi)
+    (r := itv_real2_subdef max_itv_subdef xi yi) :
+  ext_num_spec r (Order.max x%:inum y%:inum).
+Proof.
+apply: itv_real2_subproof (Itv.P x) (Itv.P y).
+case: x y => [x /= _] [y /= _] => {xi yi r} -[lx ux] [ly uy]/=.
+move=> /andP[xr /=/andP[lxx xux]] /andP[yr /=/andP[lyy yuy]].
+apply/and3P; split.
+- case: x y xr yr {lxx xux lyy yuy} => [x||] [y||]//=.
+  + by move=> ? ?; apply: comparable_maxr.
+  + by move=> ? ?; rewrite real_maxey.
+  + by move=> ? ?; rewrite real_maxNye.
+- by apply: ext_max_itv_boundl_subproof => //; apply: ereal_comparable.
+- exact: ext_max_itv_boundr_subproof.
+Qed.
+
+Canonical ext_min_max_typ (R : numDomainType) :=
+  MinMaxTyp ext_min_inum_subproof ext_max_inum_subproof.
+
+End Itv.
+
+Arguments gt0e {R i} _ {_}.
+Arguments lte0 {R i} _ {_}.
+Arguments ge0e {R i} _ {_}.
+Arguments lee0 {R i} _ {_}.
+Arguments cmp0e {R i} _ {_}.
+Arguments neqe0 {R i} _ {_}.
+Arguments ext_widen_itv {R i} _ {_ _}.
+
+Definition posnume (R : numDomainType) of phant R :=
+  Itv.def (@ext_num_sem R) (Itv.Real `]0%Z, +oo[).
+Notation "{ 'posnum' '\bar' R }" := (@posnume _ (Phant R)) : type_scope.
+Definition nonnege (R : numDomainType) of phant R :=
+  Itv.def (@ext_num_sem R) (Itv.Real `[0%Z, +oo[).
+Notation "{ 'nonneg' '\bar' R }" := (@nonnege _ (Phant R)) : type_scope.
+Notation "x %:pos" := (ext_widen_itv x%:itv : {posnum \bar _}) (only parsing)
+  : ereal_dual_scope.
+Notation "x %:pos" := (ext_widen_itv x%:itv : {posnum \bar _}) (only parsing)
+  : ereal_scope.
+Notation "x %:pos" := (@ext_widen_itv _ _
+    (@Itv.from _ _ _ (Phantom _ x)) (Itv.Real `]Posz 0, +oo[) _)
+  (only printing) : ereal_dual_scope.
+Notation "x %:pos" := (@ext_widen_itv _ _
+    (@Itv.from _ _ _ (Phantom _ x)) (Itv.Real `]Posz 0, +oo[) _)
+  (only printing) : ereal_scope.
+Notation "x %:nng" := (ext_widen_itv x%:itv : {nonneg \bar _}) (only parsing)
+  : ereal_dual_scope.
+Notation "x %:nng" := (ext_widen_itv x%:itv : {nonneg \bar _}) (only parsing)
+  : ereal_scope.
+Notation "x %:nng" := (@ext_widen_itv _ _
+    (@Itv.from _ _ _ (Phantom _ x)) (Itv.Real `[Posz 0, +oo[) _)
+  (only printing) : ereal_dual_scope.
+Notation "x %:nng" := (@ext_widen_itv _ _
+    (@Itv.from _ _ _ (Phantom _ x)) (Itv.Real `[Posz 0, +oo[) _)
+  (only printing) : ereal_scope.
+
+#[export] Hint Extern 0 (is_true (0%R < _)%E) => solve [apply: gt0e] : core.
+#[export] Hint Extern 0 (is_true (_ < 0%R)%E) => solve [apply: lte0] : core.
+#[export] Hint Extern 0 (is_true (0%R <= _)%E) => solve [apply: ge0e] : core.
+#[export] Hint Extern 0 (is_true (_ <= 0%R)%E) => solve [apply: lee0] : core.
+#[export] Hint Extern 0 (is_true (0%R >=< _)%O) => solve [apply: cmp0e] : core.
+#[export] Hint Extern 0 (is_true (_ != 0%R)%O) => solve [apply: neqe0] : core.
 
 Section MorphNum.
-Context {R : numDomainType} {nz : KnownSign.nullity} {cond : KnownSign.reality}.
-Local Notation nR := {compare (0 : \bar R) & nz & cond}.
+Context {R : numDomainType} {i : Itv.t}.
+Local Notation nR := (Itv.def (@ext_num_sem R) i).
 Implicit Types (a : \bar R).
 
 Lemma num_abse_eq0 a : (`|a|%:nng == 0%:E%:nng) = (a == 0).
@@ -3665,10 +4153,9 @@ Proof. by rewrite -abse_eq0. Qed.
 End MorphNum.
 
 Section MorphReal.
-Context {R : numDomainType} {nz : KnownSign.nullity} {r : KnownSign.real}.
-Local Notation nR := {compare (0 : \bar R) & nz & r}.
-Implicit Type x y : nR.
-Local Notation num := (@num _ _ (0 : R) nz r).
+Context {R : numDomainType} {xi yi : interval int}.
+Implicit Type x : (Itv.def (@ext_num_sem R) (Itv.Real xi)).
+Implicit Type y : (Itv.def (@ext_num_sem R) (Itv.Real yi)).
 
 Lemma num_lee_max a x y :
   a <= maxe x%:num y%:num = (a <= x%:num) || (a <= y%:num).
@@ -3703,35 +4190,6 @@ Lemma num_gte_min a x y :
 Proof. by rewrite -comparable_gt_min// ereal_comparable. Qed.
 
 End MorphReal.
-#[deprecated(since="mathcomp-analysis 1.2.0", note="renamed `num_lee_max`")]
-Notation num_lee_maxr := num_lee_max (only parsing).
-#[deprecated(since="mathcomp-analysis 1.2.0", note="renamed `num_gee_max`")]
-Notation num_lee_maxl := num_gee_max (only parsing).
-#[deprecated(since="mathcomp-analysis 1.2.0", note="renamed `num_lee_min`")]
-Notation num_lee_minr := num_lee_min (only parsing).
-#[deprecated(since="mathcomp-analysis 1.2.0", note="renamed `num_gee_min`")]
-Notation num_lee_minl := num_gee_min (only parsing).
-#[deprecated(since="mathcomp-analysis 1.2.0", note="renamed `num_lte_max`")]
-Notation num_lte_maxr := num_lte_max (only parsing).
-#[deprecated(since="mathcomp-analysis 1.2.0", note="renamed `num_gte_max`")]
-Notation num_lte_maxl := num_gte_max (only parsing).
-#[deprecated(since="mathcomp-analysis 1.2.0", note="renamed `num_lte_min`")]
-Notation num_lte_minr := num_lte_min (only parsing).
-#[deprecated(since="mathcomp-analysis 1.2.0", note="renamed `num_gte_min`")]
-Notation num_lte_minl := num_gte_min (only parsing).
-
-Section MorphGe0.
-Context {R : numDomainType} {nz : KnownSign.nullity}.
-Local Notation nR := {compare (0 : \bar R) & ?=0 & >=0}.
-Implicit Type x y : nR.
-Local Notation num := (@num _ _ (0 : \bar R) ?=0 >=0).
-
-Lemma num_abse_le a x : 0 <= a -> (`|a|%:nng <= x)%O = (a <= x%:num).
-Proof. by move=> a0; rewrite -num_le//= gee0_abs. Qed.
-
-Lemma num_abse_lt a x : 0 <= a -> (`|a|%:nng < x)%O = (a < x%:num).
-Proof. by move=> a0; rewrite -num_lt/= gee0_abs. Qed.
-End MorphGe0.
 
 Variant posnume_spec (R : numDomainType) (x : \bar R) :
   \bar R -> bool -> bool -> bool -> Type :=
@@ -3856,7 +4314,6 @@ apply: le_mono; move=> -[r0 | | ] [r1 | _ | _] //=.
 - by rewrite ltr_pdivrMr ?ltr_wpDr// mul1r ltr_pwDl // ler_norm.
 - rewrite ltr_pdivlMr ?mulN1r ?ltr_wpDr// => _.
   by rewrite ltrNl ltr_pwDl // ler_normr lexx orbT.
-- by rewrite -subr_gt0 opprK.
 Qed.
 
 Definition lt_contract := leW_mono le_contract.
diff --git a/reals/prodnormedzmodule.v b/reals/prodnormedzmodule.v
index 38bfe229c..06f7ac181 100644
--- a/reals/prodnormedzmodule.v
+++ b/reals/prodnormedzmodule.v
@@ -1,8 +1,8 @@
 (* mathcomp analysis (c) 2020 Inria and AIST. License: CeCILL-C.              *)
 From HB Require Import structures.
-From mathcomp Require Import all_ssreflect fingroup ssralg poly ssrnum. 
+From mathcomp Require Import all_ssreflect fingroup ssralg poly ssrnum.
 From mathcomp Require Import all_classical.
-From mathcomp Require Import signed.
+From mathcomp Require Import itv.
 
 (**md**************************************************************************)
 (* This file equips the product of two normedZmodTypes with a canonical       *)
diff --git a/reals/real_interval.v b/reals/real_interval.v
index 15db5ad76..1c42bc9e9 100644
--- a/reals/real_interval.v
+++ b/reals/real_interval.v
@@ -4,7 +4,7 @@ From mathcomp Require Import fingroup perm rat archimedean finmap.
 From mathcomp Require Import boolp classical_sets functions.
 From mathcomp Require Export set_interval.
 From HB Require Import structures.
-From mathcomp Require Import reals constructive_ereal signed.
+From mathcomp Require Import reals itv constructive_ereal.
 
 (**md**************************************************************************)
 (* # Sets and intervals on $\overline{\mathbb{R}}$                            *)
diff --git a/reals/signed.v b/reals/signed.v
index 84fc0d8db..93eb07f55 100644
--- a/reals/signed.v
+++ b/reals/signed.v
@@ -4,6 +4,9 @@ From Coq Require Import ssreflect ssrfun ssrbool.
 From mathcomp Require Import ssrnat eqtype choice order ssralg ssrnum ssrint.
 From mathcomp Require Import mathcomp_extra.
 
+Attributes deprecated(since="mathcomp-analysis 1.8.0",
+                      note="Use itv.v instead.").
+
 (**md**************************************************************************)
 (* # Positive, non-negative numbers, etc.                                     *)
 (*                                                                            *)
diff --git a/theories/charge.v b/theories/charge.v
index d3329dce9..241ede655 100644
--- a/theories/charge.v
+++ b/theories/charge.v
@@ -4,7 +4,7 @@ From mathcomp Require Import finmap fingroup perm rat.
 From mathcomp Require Import mathcomp_extra boolp classical_sets cardinality.
 From mathcomp Require Import functions fsbigop set_interval.
 From HB Require Import structures.
-From mathcomp Require Import reals ereal signed topology numfun normedtype.
+From mathcomp Require Import reals itv ereal topology numfun normedtype.
 From mathcomp Require Import sequences esum measure realfun lebesgue_measure.
 From mathcomp Require Import lebesgue_integral.
 
@@ -1286,7 +1286,7 @@ Qed.
 
 Lemma sup_int_approxRN_fin_num : M \is a fin_num.
 Proof.
-rewrite ge0_fin_numE//; first exact: sup_int_approxRN_lty.
+rewrite ge0_fin_numE; first exact: sup_int_approxRN_lty.
 exact: sup_int_approxRN_ge0.
 Qed.
 
@@ -1337,7 +1337,7 @@ Qed.
 
 Lemma max_approxRN_seq_ge0 n x : 0 <= F_ n x.
 Proof.
-by apply/bigmax_geP; right => /=; exists ord0 => //; exact: approxRN_seq_ge0.
+by apply/bigmax_geP; right => /=; exists ord0; [|exact: approxRN_seq_ge0].
 Qed.
 
 Lemma max_approxRN_seq_ge n x : F_ n x >= g_ n x.
@@ -1496,7 +1496,7 @@ Qed.
 
 Let F_G m : F m \in G.
 Proof.
-rewrite inE /G/=; split => //.
+rewrite inE /G/=; split.
 - by move=> ?; exact: max_approxRN_seq_ge0.
 - apply/integrableP; split; first exact: measurable_max_approxRN_seq.
   under eq_integral.
@@ -1569,7 +1569,7 @@ have [muA0|] := eqVneq (mu A) 0.
   exists (PosNum ltr01).
   under eq_integral.
     move=> x _; rewrite -(@gee0_abs _ (_ + _)); last first.
-      by rewrite adde_ge0// fRN_ge0.
+      by rewrite adde_ge0 ?fRN_ge0.
     over.
   rewrite (@integral_abs_eq0 _ _ _ _ setT)//.
     by rewrite (le_lt_trans _ h)// integral_ge0// => x Ax; exact: fRN_ge0.
@@ -1614,7 +1614,7 @@ move=> mB; rewrite ge0_integralD//; last 2 first.
   by move=> x Bx; exact: fRN_ge0.
   exact: measurable_funS measurable_fun_fRN.
 rewrite fin_numD integral_cst// fin_numM ?fin_num_measure// andbT.
-rewrite ge0_fin_numE ?measure_ge0//; last first.
+rewrite ge0_fin_numE ?measure_ge0; last first.
   by apply: integral_ge0 => x Bx; exact: fRN_ge0.
 rewrite (le_lt_trans _ int_fRN_lty)//.
 under [in leRHS]eq_integral.
@@ -1645,11 +1645,11 @@ apply: cvgeB.
   + have /cvg_ex[/= l hl] : cvg ((fun n =>
         \sum_(0 <= i < n) \int[mu]_(y in H i) (fRN y + epsRN%:num%:E)) @ \oo).
       apply: is_cvg_ereal_nneg_natsum => n _.
-      by apply: integral_ge0 => x _; rewrite adde_ge0//; exact: fRN_ge0.
+      by apply: integral_ge0 => x _; rewrite adde_ge0 ?fRN_ge0.
     by rewrite (@cvg_lim _ _ _ _ _ _ l).
   + apply: emeasurable_funD => //=; apply: measurable_funTS.
     exact: measurable_fun_fRN.
-  + by move=> x _; rewrite adde_ge0//; exact: fRN_ge0.
+  + by move=> x _; rewrite adde_ge0 ?fRN_ge0.
 Qed.
 
 HB.instance Definition _ := @isCharge.Build _ _ _ sigmaRN
@@ -1706,7 +1706,7 @@ have mh : measurable_fun setT h.
   - by apply: measurable_funTS; apply: emeasurable_funD => //; exact: mf.
   - by apply: measurable_funTS; exact: mf.
 have hge0 x : 0 <= h x.
-  by rewrite /h; case: ifPn => [_|?]; [rewrite adde_ge0// f_ge0|exact: f_ge0].
+  by rewrite /h; case: ifPn => [_|?]; rewrite ?adde_ge0 ?f_ge0.
 have hnuP S : measurable S -> S `<=` AP -> \int[mu]_(x in S) h x <= nu S.
   move=> mS SAP.
   have : 0 <= sigma S.
@@ -1746,7 +1746,7 @@ have int_h_M : \int[mu]_x h x > M.
     by rewrite setUv//; exact: mf.
     by move=> x _; exact: f_ge0.
   rewrite setUv int_fRNE -lte_subel_addl; last first.
-    rewrite ge0_fin_numE// ?sup_int_approxRN_lty//.
+    rewrite ge0_fin_numE ?sup_int_approxRN_lty.
       exact: approxRN_seq.sup_int_approxRN_lty.
     exact: sup_int_approxRN_ge0.
   by rewrite /M subee ?mule_gt0// approxRN_seq.sup_int_approxRN_fin_num.
@@ -1942,8 +1942,8 @@ have -> : \int[mu]_(x in E) (f \* g) x =
   - move=> n; apply/emeasurable_funM; apply/measurable_funTS.
       exact/measurable_EFinP.
     exact: measurable_int (f_integrable _).
-  - by move=> n x Ex //=; rewrite mule_ge0 ?lee_fin//=; exact: f_ge0.
-  - by move=> x Ex a b /ndh /= /lefP hahb; rewrite lee_wpmul2r ?lee_fin// f_ge0.
+  - by move=> n x Ex /=; rewrite mule_ge0 ?lee_fin ?f_ge0.
+  - by move=> x Ex a b /ndh /= /lefP hahb; rewrite lee_wpmul2r ?lee_fin ?f_ge0.
 suff suf n : \int[mu]_(x in E) ((EFin \o h n) x * g x) =
     \int[nu]_(x in E) (EFin \o h n) x.
   by under eq_fun do rewrite suf.
@@ -1974,7 +1974,7 @@ rewrite ge0_integralZl//.
   by rewrite -integral_mkcondr -f_integral// integral_indic// setIC.
 - apply: emeasurable_funM; first exact/measurable_EFinP.
   exact/measurable_funTS/(measurable_int _ (f_integrable _)).
-- by move=> t Et; rewrite mule_ge0// ?lee_fin//; exact: f_ge0.
+- by move=> t Et; rewrite mule_ge0 ?lee_fin ?f_ge0.
 - by move: rhn; rewrite inE => -[t _ <-]; rewrite lee_fin.
 Qed.
 
diff --git a/theories/convex.v b/theories/convex.v
index 591d0aa19..e09b544b6 100644
--- a/theories/convex.v
+++ b/theories/convex.v
@@ -2,7 +2,7 @@
 From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum finmap.
 From mathcomp Require Import matrix interval zmodp vector fieldext falgebra.
 From mathcomp Require Import mathcomp_extra boolp classical_sets set_interval.
-From mathcomp Require Import functions cardinality ereal reals signed.
+From mathcomp Require Import functions cardinality ereal reals.
 From mathcomp Require Import topology prodnormedzmodule normedtype derive.
 From mathcomp Require Import realfun itv.
 From HB Require Import structures.
diff --git a/theories/derive.v b/theories/derive.v
index fc68330d6..cdbd54a61 100644
--- a/theories/derive.v
+++ b/theories/derive.v
@@ -2,7 +2,7 @@
 From HB Require Import structures.
 From mathcomp Require Import all_ssreflect ssralg ssrnum matrix interval.
 From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
-From mathcomp Require Import reals signed topology prodnormedzmodule tvs.
+From mathcomp Require Import reals itv topology prodnormedzmodule tvs.
 From mathcomp Require Import normedtype landau forms.
 
 (**md**************************************************************************)
diff --git a/theories/ereal.v b/theories/ereal.v
index 015c0e020..2b3585f68 100644
--- a/theories/ereal.v
+++ b/theories/ereal.v
@@ -8,7 +8,7 @@ From HB Require Import structures.
 From mathcomp Require Import all_ssreflect all_algebra archimedean finmap.
 From mathcomp Require Import boolp classical_sets functions.
 From mathcomp Require Import fsbigop cardinality set_interval.
-From mathcomp Require Import reals signed topology.
+From mathcomp Require Import reals itv topology.
 From mathcomp Require Export constructive_ereal.
 
 (**md**************************************************************************)
@@ -610,47 +610,54 @@ Proof. by apply/funext => x; rewrite /= !patchE; case: ifPn. Qed.
 Section SignedRealFieldStability.
 Context {R : realFieldType}.
 
-Definition ereal_sup_reality_subdef (xnz : KnownSign.nullity)
-    (xr : KnownSign.reality) :=
-  (if KnownSign.wider_reality <=0 xr then KnownSign.Real <=0
-   else >=<0)%snum_sign.
-Arguments ereal_sup_reality_subdef /.
-
-Lemma ereal_sup_snum_subproof (xnz : KnownSign.nullity) (xr : KnownSign.reality)
-    (S : {compare (0 : \bar R) & xnz & xr} -> Prop)
-    (r := ereal_sup_reality_subdef xnz xr) :
-  Signed.spec 0 ?=0 r (ereal_sup [set x%:num | x in S]%classic).
-Proof.
-rewrite {}/r; move: xr S => [[[]|]|] S /=;
-  do ?[by apply: ub_ereal_sup => _ [? _ <-]
-      |by case: ereal_sup => [s||];
-          rewrite ?leey ?leNye// !lee_fin -realE num_real].
-Qed.
-
-Canonical ereal_sup_snum (xnz : KnownSign.nullity) (xr : KnownSign.reality)
-    (S : {compare (0 : \bar R) & xnz & xr} -> Prop) :=
-  Signed.mk (ereal_sup_snum_subproof S).
-
-Definition ereal_inf_reality_subdef (xnz : KnownSign.nullity)
-    (xr : KnownSign.reality) :=
-  (if KnownSign.wider_reality >=0 xr then KnownSign.Real >=0
-   else >=<0)%snum_sign.
-Arguments ereal_inf_reality_subdef /.
-
-Lemma ereal_inf_snum_subproof (xnz : KnownSign.nullity) (xr : KnownSign.reality)
-    (S : {compare (0 : \bar R) & xnz & xr} -> Prop)
-    (r := ereal_inf_reality_subdef xnz xr) :
-  Signed.spec 0 ?=0 r (ereal_inf [set x%:num | x in S]%classic).
-Proof.
-rewrite {}/r; move: xr S => [[[]|]|] S /=;
-  do ?[by apply: lb_ereal_inf => _ [? _ <-]
-      |by case: ereal_inf => [s||];
-          rewrite ?leey ?leNye// !lee_fin -realE num_real].
-Qed.
-
-Canonical ereal_inf_snum (xnz : KnownSign.nullity) (xr : KnownSign.reality)
-    (S : {compare (0 : \bar R) & xnz & xr} -> Prop) :=
-  Signed.mk (ereal_inf_snum_subproof S).
+Definition ereal_sup_itv_subdef (i : interval int) : interval int :=
+  let 'Interval l u := i in
+  Interval -oo%O (keep_nonpos_itv_bound_subdef u).
+Arguments ereal_sup_itv_subdef /.
+
+Lemma ereal_sup_inum_subproof i
+    (S : Itv.def (@ext_num_sem R) i -> Prop)
+    (r := itv_real1_subdef ereal_sup_itv_subdef i) :
+  Itv.spec (@ext_num_sem R) r (ereal_sup [set x%:num | x in S]%classic).
+Proof.
+rewrite {}/r; case: i S => [//| [l u]] S /=.
+apply/and3P; split.
+- rewrite real_fine -real_leey.
+  by rewrite ub_ereal_sup// => _ [[[x||] /=/and3P[? ? ?]] _ <-].
+- by case: ereal_sup.
+- case: u S => [[] [[| u] | u] S |//]; rewrite /= bnd_simp//;
+     apply: ub_ereal_sup => _ [[x /=/and3P[_ _ /= +]] _ <-]; rewrite bnd_simp//.
+  + by move/ltW.
+  + by move=> /ltW xu; apply: le_trans xu _; rewrite lee_fin lerz0.
+  + by move=> xu; apply: le_trans xu _; rewrite lee_fin lerz0.
+Qed.
+
+Canonical ereal_sup_inum i (S : Itv.def (@ext_num_sem R) i -> Prop) :=
+  Itv.mk (ereal_sup_inum_subproof S).
+
+Definition ereal_inf_itv_subdef (i : interval int) : interval int :=
+  let 'Interval l u := i in
+  Interval (keep_nonneg_itv_bound_subdef l) +oo%O.
+Arguments ereal_inf_itv_subdef /.
+
+Lemma ereal_inf_inum_subproof i
+    (S : Itv.def (@ext_num_sem R) i -> Prop)
+    (r := itv_real1_subdef ereal_inf_itv_subdef i) :
+  Itv.spec (@ext_num_sem R) r (ereal_inf [set x%:num | x in S]%classic).
+Proof.
+rewrite {}/r; case: i S => [//| [l u]] S /=.
+apply/and3P; split.
+- rewrite real_fine -real_leNye.
+  by rewrite lb_ereal_inf// => _ [[[x||] /=/and3P[? ? ?]] _ <-].
+- case: l S => [[] [l | l] S |//]; rewrite /= bnd_simp//;
+     apply: lb_ereal_inf => _ [[x /=/and3P[_ /= + _]] _ <-]; rewrite bnd_simp.
+  + by apply: le_trans; rewrite lee_fin ler0z.
+  + by move=> /ltW; apply: le_trans; rewrite lee_fin ler0z.
+- by case: ereal_inf.
+Qed.
+
+Canonical ereal_inf_inum i (S : Itv.def (@ext_num_sem R) i -> Prop) :=
+  Itv.mk (ereal_inf_inum_subproof S).
 
 End SignedRealFieldStability.
 
diff --git a/theories/esum.v b/theories/esum.v
index 57959228b..3b289711b 100644
--- a/theories/esum.v
+++ b/theories/esum.v
@@ -1,7 +1,7 @@
 (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
 From mathcomp Require Import all_ssreflect ssralg ssrnum finmap.
 From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
-From mathcomp Require Import cardinality fsbigop reals ereal signed.
+From mathcomp Require Import cardinality fsbigop reals ereal itv.
 From mathcomp Require Import topology sequences normedtype numfun.
 
 (**md**************************************************************************)
@@ -256,7 +256,7 @@ apply: (@le_trans _ _
   rewrite (fsetIidPr _).
     rewrite fsbig_finite// leeDl// big_seq sume_ge0//=.
     move=> [x y] /imfsetP[[x1 y1]] /[!inE] /andP[] /imfset2P[x2]/= /[!inE].
-    rewrite andbT in_fset_set//; last exact: finite_set_fst.
+    rewrite andbT in_fset_set; last exact: finite_set_fst.
     move=> /[!inE] x2X [y2] /[!inE] /andP[] /[!in_fset_set]; last first.
       exact: finite_set_snd.
     move=> /[!inE] y2X y2J [-> ->] _ [-> ->]; rewrite a_ge0//.
diff --git a/theories/exp.v b/theories/exp.v
index 8f709ed49..c9811ce46 100644
--- a/theories/exp.v
+++ b/theories/exp.v
@@ -2,7 +2,7 @@
 From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum matrix.
 From mathcomp Require Import interval rat.
 From mathcomp Require Import boolp classical_sets functions.
-From mathcomp Require Import mathcomp_extra reals ereal signed.
+From mathcomp Require Import mathcomp_extra reals ereal itv.
 From mathcomp Require Import topology tvs normedtype landau sequences derive.
 From mathcomp Require Import realfun itv convex.
 
diff --git a/theories/ftc.v b/theories/ftc.v
index bbc908701..27106ecba 100644
--- a/theories/ftc.v
+++ b/theories/ftc.v
@@ -2,7 +2,7 @@
 From HB Require Import structures.
 From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval finmap.
 From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
-From mathcomp Require Import cardinality fsbigop signed reals ereal.
+From mathcomp Require Import cardinality fsbigop reals itv ereal.
 From mathcomp Require Import topology tvs normedtype sequences real_interval.
 From mathcomp Require Import esum measure lebesgue_measure numfun realfun.
 From mathcomp Require Import lebesgue_integral derive charge.
diff --git a/theories/function_spaces.v b/theories/function_spaces.v
index cc56990f6..f0d714e12 100644
--- a/theories/function_spaces.v
+++ b/theories/function_spaces.v
@@ -3,7 +3,7 @@ From HB Require Import structures.
 From mathcomp Require Import all_ssreflect all_algebra finmap generic_quotient.
 From mathcomp Require Import boolp classical_sets functions.
 From mathcomp Require Import cardinality mathcomp_extra fsbigop.
-From mathcomp Require Import reals signed topology separation_axioms.
+From mathcomp Require Import reals itv topology separation_axioms.
 
 (**md**************************************************************************)
 (* # The topology of functions spaces                                         *)
diff --git a/theories/hoelder.v b/theories/hoelder.v
index b7476215d..e0f299a19 100644
--- a/theories/hoelder.v
+++ b/theories/hoelder.v
@@ -2,7 +2,7 @@
 From HB Require Import structures.
 From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval finmap.
 From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
-From mathcomp Require Import cardinality fsbigop signed reals ereal.
+From mathcomp Require Import cardinality fsbigop reals ereal.
 From mathcomp Require Import topology normedtype sequences real_interval.
 From mathcomp Require Import esum measure lebesgue_measure lebesgue_integral.
 From mathcomp Require Import numfun exp convex itv.
@@ -365,7 +365,7 @@ move=> mf mg.
 rewrite !Lnorm1 -ge0_integralD//; [|by do 2 apply: measurableT_comp..].
 rewrite ge0_le_integral//.
 - by do 2 apply: measurableT_comp => //; exact: measurable_funD.
-- by move=> x _; rewrite lee_fin.
+- by move=> x _; rewrite adde_ge0.
 - by apply/measurableT_comp/measurable_funD; exact/measurableT_comp.
 - by move=> x _; rewrite lee_fin ler_normD.
 Qed.
diff --git a/theories/kernel.v b/theories/kernel.v
index 4d154d267..0d0c0ec4d 100644
--- a/theories/kernel.v
+++ b/theories/kernel.v
@@ -2,7 +2,7 @@
 From HB Require Import structures.
 From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval finmap.
 From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
-From mathcomp Require Import cardinality fsbigop reals ereal signed.
+From mathcomp Require Import cardinality fsbigop reals itv ereal.
 From mathcomp Require Import topology normedtype sequences esum measure.
 From mathcomp Require Import numfun lebesgue_measure lebesgue_integral.
 
diff --git a/theories/landau.v b/theories/landau.v
index bee296e96..07118461b 100644
--- a/theories/landau.v
+++ b/theories/landau.v
@@ -2,7 +2,7 @@
 From HB Require Import structures.
 From mathcomp Require Import all_ssreflect ssralg ssrnum.
 From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
-From mathcomp Require Import ereal reals signed topology normedtype.
+From mathcomp Require Import ereal reals itv topology normedtype.
 From mathcomp Require Import prodnormedzmodule.
 
 (**md**************************************************************************)
@@ -480,7 +480,7 @@ Proof.
 split=> [[k k0 fOg] | [k [kreal fOg]]].
   exists k; rewrite realE (ltW k0) /=; split=> // l ltkl; move: fOg.
   by apply: filter_app; near=> x => /le_trans; apply; rewrite ler_wpM2r // ltW.
-exists (Num.max 1 `|k + 1|) => //.
+exists (Num.max 1 `|k + 1|); first exact/gt0/K.
 apply: fOg; rewrite (@lt_le_trans _ _ `|k + 1|) //.
   by rewrite (@lt_le_trans _ _ (k + 1)) ?ltrDl // real_ler_norm ?realD.
 by rewrite comparable_le_max ?real_comparable// lexx orbT.
diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v
index c9b2bbfaf..38cde5ed0 100644
--- a/theories/lebesgue_integral.v
+++ b/theories/lebesgue_integral.v
@@ -3,7 +3,7 @@ From HB Require Import structures.
 From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval finmap.
 From mathcomp Require Import archimedean.
 From mathcomp Require Import boolp classical_sets functions.
-From mathcomp Require Import cardinality fsbigop signed reals ereal topology.
+From mathcomp Require Import cardinality fsbigop reals itv ereal topology.
 From mathcomp Require Import tvs normedtype sequences real_interval esum measure.
 From mathcomp Require Import lebesgue_measure numfun realfun function_spaces.
 
@@ -1680,7 +1680,7 @@ have mh2 : measurable_fun setT h2 by exact/(measurable_restrictT _ _).1.
 have [g1 [nd_g1 gh1]] := approximation measurableT mh1 (fun x _ => h10 x).
 have [g2 [nd_g2 gh2]] := approximation measurableT mh2 (fun x _ => h20 x).
 pose g12 := fun n => add_nnsfun (g1 n) (g2 n).
-rewrite (@nd_ge0_integral_lim _ _ _ mu _ g12) //; last 3 first.
+rewrite (@nd_ge0_integral_lim _ _ _ mu _ g12); last 3 first.
   - by move=> x; rewrite adde_ge0.
   - by apply: nondecreasing_seqD => // x;
       [exact/(lef_at x nd_g1)|exact/(lef_at x nd_g2)].
@@ -1785,7 +1785,7 @@ pose Af x : set R := A `&` f @^-1` [set x].
 have mAf x : measurable (Af x) by exact: measurableI.
 have finAf x : mu (Af x) < +oo.
   by rewrite (le_lt_trans _ finA)// le_measure// ?inE//; exact: subIsetl.
-have eNpos : (0 < eps%:num/N.+1%:R)%R by [].
+have eNpos : (0 < eps%:num / N.+1%:R)%R by [].
 have dK' x := lebesgue_regularity_inner (mAf x) (finAf x) eNpos.
 pose dK x : set R := projT1 (cid (dK' x)); pose J i : set R := Af i `\` dK i.
 have dkP x := projT2 (cid (dK' x)).
@@ -3792,7 +3792,8 @@ have if_0 n : \int[mu]_(x in D) `|f_ n x| = 0.
     by apply: measurable_mine => //; exact: measurableT_comp.
   exact: f_bounded.
 rewrite (_ : (fun _ => _) = cst 0) // ?lim_cst// funeqE => n.
-by rewrite -(if_0 n); apply: eq_integral => x _; rewrite gee0_abs// /f_.
+rewrite -(if_0 n); apply: eq_integral => x _; rewrite gee0_abs// /f_.
+exact/ge0e/R.
 Unshelve. all: by end_near. Qed.
 
 Lemma integral_abs_eq0 D (N : set T) (f : T -> \bar R) :
@@ -5122,7 +5123,7 @@ have [] // := @dominated_convergence _ _ _ mu _ mE (fun n => EFin \o g_ n) f f.
 move=> _ /= fg0 gfcvg; exists g_; split.
 - move=> n; apply: (le_integrable mE _ _ intf).
     exact/measurable_EFinP/measurable_funTS.
-  move=> ? ?; rewrite /g_ !gee0_abs ?lee_fin//; last exact: fpos.
+  move=> ? ?; rewrite /g_ !gee0_abs ?lee_fin ?fpos//.
   by rewrite /= nnsfun_approxE le_approx.
 - exact: cvg_nnsfun_approx.
 - by apply: cvg_trans fg0; under eq_fun => ? do under eq_fun => t do
@@ -5451,11 +5452,11 @@ transitivity (\sum_(k \in range f)
   rewrite indic_fubini_tonelli1// -ge0_integralZl//; last by rewrite lee_fin.
   - exact: indic_measurable_fun_fubini_tonelli_F.
   - by move=> /= x _; exact: indic_fubini_tonelli_F_ge0.
-rewrite -ge0_integral_fsum //; last 2 first.
+rewrite -ge0_integral_fsum => [|//|||//]; last 2 first.
   - by move=> r; apply/measurable_funeM/indic_measurable_fun_fubini_tonelli_F.
   - move=> r x _; rewrite /fubini_F.
     have [r0|r0] := leP 0%R r.
-      by rewrite mule_ge0//; exact: indic_fubini_tonelli_F_ge0.
+      by rewrite mule_ge0 ?indic_fubini_tonelli_F_ge0.
     rewrite integral0_eq ?mule0// => y _.
     by rewrite preimage_nnfun0//= indicE in_set0.
 apply: eq_integral => x _; rewrite sfun_fubini_tonelli_FE.
@@ -5478,11 +5479,11 @@ transitivity (\sum_(k \in range f)
   rewrite indic_fubini_tonelli2// -ge0_integralZl//; last by rewrite lee_fin.
   - exact: indic_measurable_fun_fubini_tonelli_G.
   - by move=> /= x _; exact: indic_fubini_tonelli_G_ge0.
-rewrite -ge0_integral_fsum //; last 2 first.
+rewrite -ge0_integral_fsum => [|//|||//]; last 2 first.
   - by move=> r; apply/measurable_funeM/indic_measurable_fun_fubini_tonelli_G.
   - move=> r y _; rewrite /fubini_G.
     have [r0|r0] := leP 0%R r.
-      by rewrite mule_ge0//; exact: indic_fubini_tonelli_G_ge0.
+      by rewrite mule_ge0 ?indic_fubini_tonelli_G_ge0.
     rewrite integral0_eq ?mule0// => x _.
     by rewrite preimage_nnfun0//= indicE in_set0.
 apply: eq_integral => x _; rewrite sfun_fubini_tonelli_GE.
@@ -5562,7 +5563,7 @@ rewrite [LHS](_ : _ =
   set r := fun _ => _; set l := fun _ => _; have -> // : l = r.
   by apply/funext  => n; rewrite /l /r sfun_fubini_tonelli1.
 rewrite [RHS](_ : _ = limn (fun n => \int[m1]_x F_ g n x))//.
-rewrite -monotone_convergence //; first exact: eq_integral.
+rewrite -monotone_convergence => [|//|||]; first exact: eq_integral.
 - by move=> n; exact: sfun_measurable_fun_fubini_tonelli_F.
 - move=> n x _; apply: integral_ge0 => // y _ /=; rewrite lee_fin.
   exact: fun_ge0.
@@ -5596,7 +5597,7 @@ rewrite [LHS](_ : _ = limn
   set r := fun _ => _; set l := fun _ => _; have -> // : l = r.
   by apply/funext => n; rewrite /l /r sfun_fubini_tonelli sfun_fubini_tonelli2.
 rewrite [RHS](_ : _ = limn (fun n => \int[m2]_y G_ g n y))//.
-rewrite -monotone_convergence //; first exact: eq_integral.
+rewrite -monotone_convergence => [|//|||]; first exact: eq_integral.
 - by move=> n; exact: sfun_measurable_fun_fubini_tonelli_G.
 - by move=> n y _; apply: integral_ge0 => // x _ /=; rewrite lee_fin fun_ge0.
 - move=> y /= _ a b ab; apply: ge0_le_integral => //.
@@ -5730,7 +5731,7 @@ Qed.
 Let integrable_Fminus : m1.-integrable setT Fminus.
 Proof.
 apply/integrableP; split=> //.
-apply: le_lt_trans (fubini1a.1 imf); apply: ge0_le_integral => //.
+apply: le_lt_trans (fubini1a.1 imf); apply: ge0_le_integral => [//|//|||//|].
 - exact: measurableT_comp.
 - by move=> *; exact: integral_ge0.
 - move=> x _; apply: le_trans.
@@ -5848,18 +5849,18 @@ transitivity (\sum_(n <oo) \int[s1 n]_x \sum_(m <oo) \int[s2 m]_y f (x, y)).
   apply: eq_eseriesr => n _; apply: eq_integral => x _.
   by rewrite ge0_integral_measure_series//; exact/measurableT_comp.
 transitivity (\sum_(n <oo) \sum_(m <oo) \int[s1 n]_x \int[s2 m]_y f (x, y)).
-  apply: eq_eseriesr => n _; rewrite integral_nneseries//.
+  apply: eq_eseriesr => n _; rewrite integral_nneseries => [//|//||].
     by move=> m; exact: measurable_fun_fubini_tonelli_F.
   by move=> m x _; exact: integral_ge0.
 transitivity (\sum_(n <oo) \sum_(m <oo) \int[s2 m]_y \int[s1 n]_x f (x, y)).
   apply: eq_eseriesr => n _; apply: eq_eseriesr => m _.
   by rewrite fubini_tonelli//; exact: finite_measure_sigma_finite.
 transitivity (\sum_(n <oo) \int[mseries s2 0]_y \int[s1 n]_x f (x, y)).
-  apply: eq_eseriesr => n _; rewrite ge0_integral_measure_series//.
+  apply: eq_eseriesr => n _; rewrite ge0_integral_measure_series => [//|//||].
     by move=> y _; exact: integral_ge0.
   exact: measurable_fun_fubini_tonelli_G.
 transitivity (\int[mseries s2 0]_y \sum_(n <oo) \int[s1 n]_x f (x, y)).
-  rewrite integral_nneseries//.
+  rewrite integral_nneseries => [//|//||].
     by move=> n; apply: measurable_fun_fubini_tonelli_G.
   by move=> n y _; exact: integral_ge0.
 transitivity (\int[mseries s2 0]_y \int[mseries s1 0]_x f (x, y)).
@@ -6125,7 +6126,7 @@ Proof.
 move=> Df x; apply: ereal_sup_le => //=.
 pose k := \int[mu]_(x in D `&` ball x 1) `|f x|%:E.
 exists ((fine (mu (ball x 1)))^-1%:E * k); last first.
-  rewrite mule_ge0//; last exact: integral_ge0.
+  rewrite mule_ge0 ?integral_ge0//.
   by rewrite lee_fin// invr_ge0// fine_ge0.
 exists 1%R; first by rewrite in_itv/= ltr01.
 rewrite iavg_restrict//; last exact: measurable_ball.
@@ -6190,7 +6191,7 @@ move: a0; rewrite le_eqVlt => /predU1P[a0|a0].
 have ka_pos : fine k / a \is Num.pos.
   by rewrite posrE divr_gt0// fine_gt0 // k_gt0/= locally_integrable_ltbally.
 have k_fin_num : k \is a fin_num.
-  by rewrite ge0_fin_numE ?locally_integrable_ltbally// integral_ge0.
+  by rewrite ge0_fin_numE ?locally_integrable_ltbally ?integral_ge0.
 have kar : (0 < 2^-1 * (fine k / a) - r)%R.
   move: afxr; rewrite -{1}(fineK k_fin_num) -lte_pdivrMr; last first.
     by rewrite fine_gt0// k_gt0/= ltey_eq k_fin_num.
@@ -6292,7 +6293,7 @@ apply: (@le_trans _ _
     (\sum_(i <- E) c^-1%:E * \int[mu]_(y in B i) `|(f y)|%:E)).
   rewrite [in leLHS]big_seq [in leRHS]big_seq; apply: lee_sum => r /ED /Dsub /[!inE] rD.
   by rewrite -lee_pdivrMl ?invr_gt0// invrK /B/=; exact/ltW/cMfx_int.
-rewrite -ge0_sume_distrr//; last by move=> x _; rewrite integral_ge0.
+rewrite -ge0_sume_distrr; last by move=> x _; rewrite integral_ge0.
 rewrite lee_wpmul2l//; first by rewrite lee_fin invr_ge0 ltW.
 rewrite -ge0_integral_bigsetU//=.
 - apply: ge0_subset_integral => //.
diff --git a/theories/lebesgue_measure.v b/theories/lebesgue_measure.v
index 5fbc202ca..56cc49a89 100644
--- a/theories/lebesgue_measure.v
+++ b/theories/lebesgue_measure.v
@@ -2,7 +2,7 @@
 From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval.
 From mathcomp Require Import finmap fingroup perm rat archimedean.
 From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
-From mathcomp Require Import cardinality fsbigop reals ereal signed.
+From mathcomp Require Import cardinality fsbigop reals itv ereal.
 From mathcomp Require Import topology numfun tvs normedtype function_spaces.
 From HB Require Import structures.
 From mathcomp Require Import sequences esum measure real_interval realfun exp.
@@ -1693,7 +1693,8 @@ apply/uniform_restrict_cvg => /= U /=; rewrite !uniform_nbhsT.
 case/nbhs_ex => del /= ballU; apply: filterS; first by move=> ?; exact: ballU.
 have [N _ /(_ N)/(_ (leqnn _)) Ndel] := near_infty_natSinv_lt del.
 exists (badn N) => // r badNr x.
-rewrite /patch; case: ifPn => // /set_mem xAB; apply: (lt_trans _ Ndel).
+rewrite /patch; case: ifPn; last by move=> ?; apply: ballxx.
+move=> /[!inE] xAB; apply: (lt_trans _ Ndel).
 move: xAB; rewrite setDE => -[Ax]; rewrite setC_bigcup => /(_ N I).
 rewrite /E setC_bigcup => /(_ r) /=; rewrite /h => /(_ badNr) /not_andP[]//.
 by move/negP; rewrite ltNge // distrC.
@@ -2493,7 +2494,7 @@ have [|Aoo e0] := leP +oo (l^* A)%mu.
   by exists [set: R]; split => //; [exact: openT|rewrite Aoo leey].
 have [F AF Fe] : exists2 I_, open_itv_cover A I_ &
     \sum_(0 <= k <oo) l (I_ k) <= (l^* A)%mu + e%:E.
-  have : (l^* A)%mu\is a fin_num by rewrite ge0_fin_numE// outer_measure_ge0.
+  have : (l^* A)%mu\is a fin_num by rewrite ge0_fin_numE ?outer_measure_ge0.
   rewrite outer_measure_open_itv_cover.
   move=> /lb_ereal_inf_adherent-/(_ _ e0)[_/= [F]] AF <- Fe.
   by exists F => //; exact/ltW.
diff --git a/theories/lebesgue_stieltjes_measure.v b/theories/lebesgue_stieltjes_measure.v
index 9e05ac8e7..f3fb9106d 100644
--- a/theories/lebesgue_stieltjes_measure.v
+++ b/theories/lebesgue_stieltjes_measure.v
@@ -4,7 +4,7 @@ From mathcomp Require Import finmap fingroup perm rat archimedean.
 From HB Require Import structures.
 From mathcomp.classical Require Import mathcomp_extra boolp classical_sets.
 From mathcomp.classical Require Import functions fsbigop cardinality.
-From mathcomp Require Import reals ereal signed topology numfun normedtype.
+From mathcomp Require Import reals ereal itv topology numfun normedtype.
 From mathcomp Require Import sequences esum real_interval measure realfun.
 
 (**md**************************************************************************)
diff --git a/theories/measure.v b/theories/measure.v
index 6cfd34f05..fd92ca66b 100644
--- a/theories/measure.v
+++ b/theories/measure.v
@@ -1,7 +1,7 @@
 (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
 From mathcomp Require Import all_ssreflect all_algebra archimedean finmap.
 From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
-From mathcomp Require Import cardinality fsbigop reals ereal signed.
+From mathcomp Require Import cardinality fsbigop reals itv ereal.
 From mathcomp Require Import topology normedtype sequences esum numfun.
 From HB Require Import structures.
 
@@ -1967,10 +1967,16 @@ Context d (T : semiRingOfSetsType d) (R : numFieldType).
 
 Variable mu : {content set T -> \bar R}.
 
-Lemma content_snum_subproof S : Signed.spec 0 ?=0 >=0 (mu S).
-Proof. exact: measure_ge0. Qed.
+Lemma content_inum_subproof S :
+  Itv.spec (@ext_num_sem R) (Itv.Real `[0%Z, +oo[) (mu S).
+Proof.
+apply/and3P; split.
+- by rewrite real_fine -real_leNye; apply: le_trans (measure_ge0 _ _).
+- by rewrite /= bnd_simp measure_ge0.
+- by rewrite bnd_simp.
+Qed.
 
-Canonical content_snum S := Signed.mk (content_snum_subproof S).
+Canonical content_inum S := Itv.mk (content_inum_subproof S).
 
 End content_signed.
 
@@ -2121,10 +2127,16 @@ Context d (R : numFieldType) (T : semiRingOfSetsType d).
 
 Variable mu : {measure set T -> \bar R}.
 
-Lemma measure_snum_subproof S : Signed.spec 0 ?=0 >=0 (mu S).
-Proof. exact: measure_ge0. Qed.
+Lemma measure_inum_subproof S :
+  Itv.spec (@ext_num_sem R) (Itv.Real `[0%Z, +oo[) (mu S).
+Proof.
+apply/and3P; split.
+- by rewrite real_fine -real_leNye; apply: le_trans (measure_ge0 _ _).
+- by rewrite /= bnd_simp measure_ge0.
+- by rewrite bnd_simp.
+Qed.
 
-Canonical measure_snum S := Signed.mk (measure_snum_subproof S).
+Canonical measure_inum S := Itv.mk (measure_inum_subproof S).
 
 End measure_signed.
 
@@ -3563,7 +3575,7 @@ by rewrite /mnormalize; case: ifPn => // _; rewrite measure0 mul0e.
 Qed.
 
 Let mnormalize_ge0 U : 0 <= mnormalize U.
-Proof. by rewrite /mnormalize; case: ifPn => //; case: ifPn. Qed.
+Proof. by rewrite /mnormalize; case: ifPn. Qed.
 
 Let mnormalize_sigma_additive : semi_sigma_additive mnormalize.
 Proof.
diff --git a/theories/normedtype.v b/theories/normedtype.v
index bf18d7bcd..b47d8d0f7 100644
--- a/theories/normedtype.v
+++ b/theories/normedtype.v
@@ -5,10 +5,9 @@ From mathcomp Require Import rat interval zmodp vector fieldext falgebra.
 From mathcomp Require Import boolp classical_sets functions.
 From mathcomp Require Import archimedean.
 From mathcomp Require Import cardinality set_interval ereal reals.
-From mathcomp Require Import signed topology prodnormedzmodule function_spaces.
+From mathcomp Require Import itv topology prodnormedzmodule function_spaces.
 From mathcomp Require Export real_interval separation_axioms tvs.
 
-
 (**md**************************************************************************)
 (* # Norm-related Notions                                                     *)
 (*                                                                            *)
@@ -2341,7 +2340,7 @@ rewrite /normr /ball_ predeq3E => x e y /=; rewrite mx_normE; split => xey.
   by rewrite -num_lt /=; split => // -[? ?] _; rewrite !mxE; exact: xey.
 - have e_gt0 : 0 < e by rewrite (le_lt_trans _ xey).
   move: e_gt0 (e_gt0) xey => /ltW/nonnegP[{}e] e_gt0.
-  move=> /(bigmax_ltP _ _ _ (fun _ => _%:sgn)) /= [e0 xey] i j.
+  move=> /(bigmax_ltP _ _ _ (fun _ => _%:itv)) /= [e0 xey] i j.
   by move: (xey (i, j)); rewrite !mxE; exact.
 Qed.
 
@@ -3311,7 +3310,8 @@ rewrite ball_close; split=> [bxy|edist0 eps]; first last.
   by apply: (@edist_lt_ball _ (x, y)); rewrite edist0.
 case: ltgtP (edist_ge0 (x, y)) => // dpos _.
 have xxfin : edist (x, y) \is a fin_num.
-  by rewrite ge0_fin_numE// (@le_lt_trans _ _ 1%:E) ?ltey// edist_fin.
+  rewrite ge0_fin_numE// (@le_lt_trans _ _ 1%:E) ?ltey// edist_fin//.
+  exact: bxy (widen_itv 1%:itv).
 have dpose : fine (edist (x, y)) > 0 by rewrite -lte_fin fineK.
 pose eps := PosNum dpose.
 have : (edist (x, y) <= (eps%:num / 2)%:E)%E.
@@ -5330,7 +5330,7 @@ Proof.
 split=> [/nbhs_ballP[_/posnumP[r] xrB]|[e xeB]]; last first.
   apply/nbhs_ballP; exists e%:num => //=.
   exact: (subset_trans (@subset_closure _ _) xeB).
-exists (r%:num / 2)%:sgn.
+exists (r%:num / 2)%:itv.
 apply: (subset_trans (closed_ball_subset _ _) xrB) => //=.
 by rewrite lter_pdivrMr // ltr_pMr // ltr1n.
 Qed.
diff --git a/theories/numfun.v b/theories/numfun.v
index f3361cce0..4be9731cc 100644
--- a/theories/numfun.v
+++ b/theories/numfun.v
@@ -2,7 +2,7 @@
 From HB Require Import structures.
 From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval finmap.
 From mathcomp Require Import mathcomp_extra boolp classical_sets fsbigop.
-From mathcomp Require Import functions cardinality set_interval signed reals.
+From mathcomp Require Import functions cardinality set_interval itv reals.
 From mathcomp Require Import ereal topology normedtype sequences.
 From mathcomp Require Import function_spaces.
 
diff --git a/theories/probability.v b/theories/probability.v
index c57cac324..3805178f0 100644
--- a/theories/probability.v
+++ b/theories/probability.v
@@ -5,7 +5,7 @@ From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
 From mathcomp Require Import cardinality fsbigop.
 From HB Require Import structures.
 From mathcomp Require Import exp numfun lebesgue_measure lebesgue_integral.
-From mathcomp Require Import reals ereal signed topology normedtype sequences.
+From mathcomp Require Import reals itv ereal topology normedtype sequences.
 From mathcomp Require Import esum measure exp numfun lebesgue_measure.
 From mathcomp Require Import lebesgue_integral kernel.
 
@@ -924,7 +924,7 @@ Context {R : realType}.
 Variables (p : R) (p0 : (0 <= p)%R) (p1 : ((NngNum p0)%:num <= 1)%R).
 
 Lemma bernoulli_dirac : bernoulli p = measure_add
-  (mscale (NngNum p0) \d_true) (mscale (onem_nonneg p1) \d_false).
+  (mscale (NngNum p0) \d_true) (mscale (1 - (Itv01 p0 p1)%:num)%:nng \d_false).
 Proof.
 apply/funext => U; rewrite /bernoulli; case: ifPn => [p01|]; last first.
   by rewrite p0/= p1.
diff --git a/theories/realfun.v b/theories/realfun.v
index b11415d1c..de0b66aff 100644
--- a/theories/realfun.v
+++ b/theories/realfun.v
@@ -4,7 +4,7 @@ From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum archimedean.
 From mathcomp Require Import matrix interval zmodp vector fieldext falgebra.
 From mathcomp Require Import finmap.
 From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
-From mathcomp Require Import cardinality ereal reals signed.
+From mathcomp Require Import cardinality ereal reals itv.
 From mathcomp Require Import topology prodnormedzmodule tvs normedtype derive.
 From mathcomp Require Import sequences real_interval.
 
diff --git a/theories/separation_axioms.v b/theories/separation_axioms.v
index 89a01e9d6..b2084deea 100644
--- a/theories/separation_axioms.v
+++ b/theories/separation_axioms.v
@@ -4,7 +4,7 @@ From mathcomp Require Import all_ssreflect all_algebra finmap generic_quotient.
 From mathcomp Require Import archimedean.
 From mathcomp Require Import boolp classical_sets functions wochoice.
 From mathcomp Require Import cardinality mathcomp_extra fsbigop set_interval.
-From mathcomp Require Import filter reals signed topology.
+From mathcomp Require Import filter reals itv topology.
 
 (**md**************************************************************************)
 (* # Separation Axioms                                                        *)
diff --git a/theories/sequences.v b/theories/sequences.v
index a3017a06d..2085b1e55 100644
--- a/theories/sequences.v
+++ b/theories/sequences.v
@@ -3,7 +3,7 @@ From HB Require Import structures.
 From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum matrix.
 From mathcomp Require Import interval rat archimedean.
 From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
-From mathcomp Require Import set_interval reals ereal signed topology.
+From mathcomp Require Import set_interval reals itv ereal topology.
 From mathcomp Require Import tvs normedtype landau.
 
 (**md**************************************************************************)
@@ -892,7 +892,7 @@ suff abel : forall n,
     rewrite a_o.
     set h := 'o_\oo (@harmonic R).
     apply/eqoP => _/posnumP[e] /=.
-    near=> n; rewrite normr1 mulr1 normrM -ler_pdivlMl// ?normr_gt0//.
+    near=> n; rewrite normr1 mulr1 normrM -ler_pdivlMl ?normr_gt0//.
     rewrite mulrC -normrV ?unitfE //.
     near: n.
     by case: (eqoP eventually_filterType (@harmonic R) h) => Hh _; apply Hh.
@@ -2855,8 +2855,9 @@ have /le_trans -> // : `| y n - y (n + m)| <=
   rewrite (le_trans (ler_distD (y (n + m)%N) _ _))//.
   apply: (le_trans (lerD ih _)); first by rewrite distrC addnS; exact: f1.
   rewrite [_ * `|_|]mulrC exprD mulrA geometric_seriesE ?lt_eqF//=.
-  rewrite -!/(`1-_) (onem_PosNum ctrf.1) (onemX_NngNum (ltW ctrf.1)).
-  rewrite -!mulrA -mulrDr ler_pM// -mulrDr exprSr onemM -addrA.
+  pose q' := Itv01 (!! ge0 q) (ltW q1).
+  rewrite -[q%:num]/(q'%:num) -!mulrA -mulrDr ler_pM// {}/q'/=.
+  rewrite -!/(`1-_) -mulrDr exprSr onemM -addrA.
   rewrite -[in leRHS](mulrC _ `1-(_ ^+ m)) -onemMr onemK.
   by rewrite [in leRHS]mulrDl mulrAC mulrV ?mul1r// unitf_gt0// onem_gt0.
 rewrite geometric_seriesE ?lt_eqF//= -[leRHS]mulr1 (ACl (1*4*2*3))/= -/C.
@@ -2951,7 +2952,7 @@ have Ar : forall na : nat * (U * {posnum K}), exists b : U * {posnum K},
   have /open_nbhs_nbhs/nbhs_closedballP[rn01 Ball_an1] :
     open_nbhs an1 ((closed_ball an rn%:num)^° `&` F n.+1) by [].
   have n31_gt0 : n.+3%:R^-1 > 0 :> K by [].
-  have majr : minr (PosNum n31_gt0)%:num rn01%:num > 0 by [].
+  have majr : minr (PosNum n31_gt0)%:num rn01%:num > 0 by exact/gt0/K.
   exists (an1, PosNum majr); split.
     apply/(subset_trans _ Ball_an1)/le_closed_ball => /=.
     by rewrite ge_min lexx orbT.
diff --git a/theories/topology_theory/compact.v b/theories/topology_theory/compact.v
index f0187e8a1..321dd2a07 100644
--- a/theories/topology_theory/compact.v
+++ b/theories/topology_theory/compact.v
@@ -1,7 +1,7 @@
 (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
 From HB Require Import structures.
 From mathcomp Require Import all_ssreflect all_algebra finmap all_classical.
-From mathcomp Require Import signed reals topology_structure uniform_structure.
+From mathcomp Require Import itv reals topology_structure uniform_structure.
 From mathcomp Require Import pseudometric_structure.
 
 (**md**************************************************************************)
diff --git a/theories/topology_theory/matrix_topology.v b/theories/topology_theory/matrix_topology.v
index 7610383a1..09e67f1b2 100644
--- a/theories/topology_theory/matrix_topology.v
+++ b/theories/topology_theory/matrix_topology.v
@@ -1,7 +1,7 @@
 (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
 From HB Require Import structures.
 From mathcomp Require Import all_ssreflect all_algebra finmap all_classical.
-From mathcomp Require Import signed topology_structure uniform_structure.
+From mathcomp Require Import itv topology_structure uniform_structure.
 From mathcomp Require Import pseudometric_structure.
 (**md**************************************************************************)
 (* # Matrix topology                                                          *)
diff --git a/theories/topology_theory/num_topology.v b/theories/topology_theory/num_topology.v
index ea87ef618..5685a0dc0 100644
--- a/theories/topology_theory/num_topology.v
+++ b/theories/topology_theory/num_topology.v
@@ -2,7 +2,7 @@
 From HB Require Import structures.
 From mathcomp Require Import all_ssreflect all_algebra archimedean.
 From mathcomp Require Import all_classical.
-From mathcomp Require Import signed reals topology_structure uniform_structure.
+From mathcomp Require Import itv reals topology_structure uniform_structure.
 From mathcomp Require Import pseudometric_structure order_topology.
 
 (**md**************************************************************************)
diff --git a/theories/topology_theory/product_topology.v b/theories/topology_theory/product_topology.v
index 4755458fc..08e77020b 100644
--- a/theories/topology_theory/product_topology.v
+++ b/theories/topology_theory/product_topology.v
@@ -1,7 +1,7 @@
 (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
 From HB Require Import structures.
 From mathcomp Require Import all_ssreflect all_algebra all_classical.
-From mathcomp Require Import signed topology_structure uniform_structure.
+From mathcomp Require Import itv topology_structure uniform_structure.
 From mathcomp Require Import pseudometric_structure compact.
 
 (**md**************************************************************************)
diff --git a/theories/topology_theory/pseudometric_structure.v b/theories/topology_theory/pseudometric_structure.v
index ec133325f..fd98cbf4a 100644
--- a/theories/topology_theory/pseudometric_structure.v
+++ b/theories/topology_theory/pseudometric_structure.v
@@ -2,7 +2,7 @@
 From HB Require Import structures.
 From mathcomp Require Import all_ssreflect all_algebra archimedean.
 From mathcomp Require Import all_classical.
-From mathcomp Require Import signed reals topology_structure uniform_structure.
+From mathcomp Require Import itv reals topology_structure uniform_structure.
 
 (**md**************************************************************************)
 (* # PseudoMetric Spaces                                                      *)
diff --git a/theories/topology_theory/weak_topology.v b/theories/topology_theory/weak_topology.v
index 0b13ca98d..290970716 100644
--- a/theories/topology_theory/weak_topology.v
+++ b/theories/topology_theory/weak_topology.v
@@ -1,7 +1,7 @@
 (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
 From HB Require Import structures.
 From mathcomp Require Import all_ssreflect all_algebra all_classical.
-From mathcomp Require Import signed reals topology_structure uniform_structure.
+From mathcomp Require Import itv reals topology_structure uniform_structure.
 From mathcomp Require Import order_topology pseudometric_structure.
 
 (**md**************************************************************************)
diff --git a/theories/trigo.v b/theories/trigo.v
index 90a2d0435..7474e66b9 100644
--- a/theories/trigo.v
+++ b/theories/trigo.v
@@ -3,7 +3,7 @@ From HB Require Import structures.
 From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum matrix.
 From mathcomp Require Import interval rat.
 From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
-From mathcomp Require Import reals ereal nsatz_realtype signed topology.
+From mathcomp Require Import reals ereal nsatz_realtype itv topology.
 From mathcomp Require Import normedtype landau sequences derive realfun exp.
 
 (**md**************************************************************************)
diff --git a/theories/tvs.v b/theories/tvs.v
index cb5c93eaf..98bc52663 100644
--- a/theories/tvs.v
+++ b/theories/tvs.v
@@ -4,7 +4,7 @@ From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum finmap matrix.
 From mathcomp Require Import rat interval zmodp vector fieldext falgebra.
 From mathcomp Require Import archimedean.
 From mathcomp Require Import boolp classical_sets functions cardinality.
-From mathcomp Require Import set_interval ereal reals signed topology.
+From mathcomp Require Import set_interval ereal reals itv topology.
 From mathcomp Require Import prodnormedzmodule function_spaces.
 From mathcomp Require Import separation_axioms.