diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index b27e544cf..272348558 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -27,6 +27,15 @@
   + lemma `FTC1` (specialization of the previous `FTC1` lemma, now renamed to `FTC1_lebesgue_pt`)
   + lemma `FTC1Ny`
 
+- in `reals.v`:
+  + lemma `mem_rg1_floor`
+
+- in `mathcomp_extra.v`:
+  + lemma `ge_floor`
+
+- in `mathcomp_extra.v`:
+  + lemmas `intr1D`, `intrD1`, `floor_eq`, `floorN`
+
 ### Changed
 
 - in `topology.v`:
@@ -34,6 +43,21 @@
     `subspace_pm_ball_triangle`, `subspace_pm_entourage` turned
 	into local `Let`'s
 
+- in `reals.v`:
+  + definitions `Rceil`, `Rfloor`
+
+- moved from `reals.v` to `mathcomp_extra.v`
+  + lemma `lt_succ_floor`: conclusion changed to match `lt_succ_floor` in MathComp,
+    generalized to `archiDomainType`
+  + generalized to `archiDomainType`:
+    lemmas `floor_ge0`, `floor_lt0`, `floor_natz`,
+    `floor_ge_int`, `floor_neq0`, `floor_lt_int`, `ceil_ge`, `ceil_ge0`, `ceil_gt0`,
+    `ceil_le0`, `ceil_ge_int`, `ceilN`, `abs_ceil_ge`
+  + generalized to `archiDomainType` and precondition generalized:
+    * `floor_le0`
+  + generalized to `archiDomainType` and renamed:
+    * `ceil_lt_int` -> `ceil_gt_int`
+
 ### Renamed
 
 - in `constructive_ereal.v`:
@@ -62,8 +86,19 @@
 
 ### Deprecated
 
+- in `reals.v`:
+  + `floor_le` (use `ge_floor` instead)
+  + `le_floor` (use `Num.Theory.floor_le` instead)
+  + `le_ceil` (use `ceil_ge` instead)
+
 ### Removed
 
+- in `reals.v`:
+  + definition `floor` (use `Num.floor` instead)
+  + definition `ceil` (use `Num.ceil` instead)
+  + lemmas `floor0`, `floor1`
+  + lemma `le_floor` (use `Num.Theory.floor_le` instead)
+
 ### Infrastructure
 
 ### Misc
diff --git a/classical/mathcomp_extra.v b/classical/mathcomp_extra.v
index 0e82043f4..c4338dd58 100644
--- a/classical/mathcomp_extra.v
+++ b/classical/mathcomp_extra.v
@@ -374,3 +374,83 @@ by elim: p => //= p <-;
 Qed.
 
 End positive.
+
+Lemma intrD1 {R : ringType} (i : int) : i%:~R + 1 = (i + 1)%:~R :> R.
+Proof. by rewrite intrD. Qed.
+
+Lemma intr1D {R : ringType} (i : int) : 1 + i%:~R = (1 + i)%:~R :> R.
+Proof. by rewrite intrD. Qed.
+
+From mathcomp Require Import archimedean.
+
+Section floor_ceil.
+Context {R : archiDomainType}.
+Implicit Type x : R.
+
+Lemma ge_floor x : (Num.floor x)%:~R <= x.
+Proof. exact: Num.Theory.ge_floor. Qed.
+
+Lemma floor_ge_int x (z : int) : (z%:~R <= x) = (z <= Num.floor x).
+Proof. exact: Num.Theory.floor_ge_int. Qed.
+
+Lemma floor_lt_int x (z : int) : (x < z%:~R) = (Num.floor x < z).
+Proof. by rewrite ltNge floor_ge_int -ltNge. Qed.
+
+Lemma floor_ge0 x : (0 <= Num.floor x) = (0 <= x).
+Proof. by rewrite -floor_ge_int. Qed.
+
+Lemma floor_le0 x : (x < 1) = (Num.floor x <= 0).
+Proof. by rewrite -ltzD1 add0r -floor_lt_int. Qed.
+
+Lemma floor_lt0 x : (x < 0) = (Num.floor x < 0).
+Proof. by rewrite -floor_lt_int. Qed.
+
+Lemma lt_succ_floor x : x < (Num.floor x + 1)%:~R.
+Proof. exact: Num.Theory.lt_succ_floor. Qed.
+
+Lemma floor_eq x m : (Num.floor x == m) = (m%:~R <= x < (m + 1)%:~R).
+Proof.
+apply/eqP/idP; [move=> <-|by move=> /Num.Theory.floor_def ->].
+by rewrite Num.Theory.ge_floor//= Num.Theory.lt_succ_floor.
+Qed.
+
+Lemma floor_neq0 x : (Num.floor x != 0) = (x < 0) || (x >= 1).
+Proof. by rewrite neq_lt -floor_lt_int gtz0_ge1 -floor_ge_int. Qed.
+
+#[deprecated(since="mathcomp-analysis 1.3.0", note="use `Num.Theory.le_ceil` instead")]
+Lemma ceil_ge x : x <= (Num.ceil x)%:~R.
+Proof. exact: Num.Theory.le_ceil. Qed.
+
+#[deprecated(since="mathcomp-analysis 1.3.0", note="use `Num.Theory.ceil_le_int`")]
+Lemma ceil_ge_int x (z : int) : (x <= z%:~R) = (Num.ceil x <= z).
+Proof. exact: Num.Theory.ceil_le_int. Qed.
+
+Lemma ceil_gt_int x (z : int) : (z%:~R < x) = (z < Num.ceil x).
+Proof. by rewrite ltNge Num.Theory.ceil_le_int// -ltNge. Qed.
+
+Lemma ceilN x : Num.ceil (- x) = - Num.floor x.
+Proof. by rewrite /Num.ceil opprK. Qed.
+
+Lemma floorN x : Num.floor (- x) = - Num.ceil x.
+Proof. by rewrite /Num.ceil opprK. Qed.
+
+Lemma ceil_ge0 x : (- 1 < x) = (0 <= Num.ceil x).
+Proof. by rewrite ltrNl floor_le0 floorN lerNl oppr0. Qed.
+
+Lemma ceil_gt0 x : (0 < x) = (0 < Num.ceil x).
+Proof. by rewrite -ceil_gt_int. Qed.
+
+Lemma ceil_le0 x : (x <= 0) = (Num.ceil x <= 0).
+Proof. by rewrite -Num.Theory.ceil_le_int. Qed.
+
+Lemma abs_ceil_ge x : `|x| <= `|Num.ceil x|.+1%:R.
+Proof.
+rewrite -natr1 natr_absz; have [x0|x0] := ltP 0 x.
+  by rewrite !gtr0_norm// -?ceil_gt0// (le_trans (Num.Theory.le_ceil _))// lerDl.
+by rewrite !ler0_norm -?ceil_le0// opprK intrD1 ltW// lt_succ_floor.
+Qed.
+
+End floor_ceil.
+
+#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed to `ceil_gt_int`")]
+Notation ceil_lt_int := ceil_gt_int (only parsing).
diff --git a/theories/Rstruct.v b/theories/Rstruct.v
index 50a515281..903d00db6 100644
--- a/theories/Rstruct.v
+++ b/theories/Rstruct.v
@@ -29,6 +29,7 @@ Require Import Rdefinitions Raxioms RIneq Rbasic_fun Zwf.
 Require Import Epsilon FunctionalExtensionality Ranalysis1 Rsqrt_def.
 Require Import Rtrigo1 Reals.
 From mathcomp Require Import all_ssreflect ssralg poly mxpoly ssrnum.
+From mathcomp Require Import archimedean.
 From HB Require Import structures.
 From mathcomp Require Import mathcomp_extra.
 
@@ -87,7 +88,7 @@ Proof. by move=> *; rewrite Rplus_assoc. Qed.
 HB.instance Definition _ := GRing.isZmodule.Build R
   RplusA Rplus_comm Rplus_0_l Rplus_opp_l.
 
-Fact RmultA : associative (Rmult).
+Fact RmultA : associative Rmult.
 Proof. by move=> *; rewrite Rmult_assoc. Qed.
 
 Fact R1_neq_0 : R1 != R0.
@@ -292,7 +293,7 @@ rewrite /Rminus Rplus_assoc [- _ + _]Rplus_comm -Rplus_assoc -!/(Rminus _ _).
 exact: Rle_minus.
 Qed.
 
-HB.instance Definition _ := Num.RealField_isArchimedean.Build R
+HB.instance Definition _ := Num.NumDomain_bounded_isArchimedean.Build R
   Rarchimedean_axiom.
 
 (** Here are the lemmas that we will use to prove that R has
diff --git a/theories/altreals/realsum.v b/theories/altreals/realsum.v
index c5eac8ae6..900f467ce 100644
--- a/theories/altreals/realsum.v
+++ b/theories/altreals/realsum.v
@@ -2,12 +2,11 @@
 (* Copyright (c) - 2015--2016 - IMDEA Software Institute                *)
 (* Copyright (c) - 2015--2018 - Inria                                   *)
 (* Copyright (c) - 2016--2018 - Polytechnique                           *)
-
 (* -------------------------------------------------------------------- *)
-From mathcomp Require Import all_ssreflect all_algebra.
+From mathcomp Require Import all_ssreflect all_algebra archimedean.
 From mathcomp.classical Require Import boolp.
 Require Import xfinmap ereal reals discrete realseq.
-From mathcomp.classical Require Import classical_sets functions mathcomp_extra.
+From mathcomp.classical Require Import classical_sets functions.
 Require Import topology.
 
 Set Implicit Arguments.
@@ -16,6 +15,7 @@ Unset Printing Implicit Defensive.
 Unset SsrOldRewriteGoalsOrder.
 
 Import Order.TTheory GRing.Theory Num.Theory.
+From mathcomp.classical Require Import mathcomp_extra.
 
 Local Open Scope fset_scope.
 Local Open Scope ring_scope.
@@ -141,28 +141,24 @@ Lemma summable_countn0 : summable f -> countable [pred x | f x != 0].
 Proof.
 case/summableP=> M ge0_M bM; pose E (p : nat) := [pred x | `|f x| > 1 / p.+1%:~R].
 set F := [pred x | _]; have le: {subset F <= [pred x | `[< exists p, x \in E p >]]}.
-  move=> x; rewrite !inE => nz_fx.
-  pose j := `|floor (1 / `|f x|)|%N; exists j; rewrite inE.
-  rewrite ltr_pdivrMr ?ltr0z // -ltr_pdivrMl ?normr_gt0 //.
-  rewrite mulr1 /j div1r -addn1 /= PoszD intrD mulr1z.
-  rewrite gez0_abs ?floor_ge0 ?invr_ge0 ?normr_ge0 //.
-  by rewrite -RfloorE; apply lt_succ_Rfloor.
+  move=> x; rewrite !inE => nz_fx; exists (Num.trunc `|f x|^-1).
+  rewrite inE mul1r invf_plt ?unfold_in /= ?normr_gt0 //.
+  by have/trunc_itv/andP[]: 0 <= `|f x|^-1 by rewrite invr_ge0 normr_ge0.
 apply/(countable_sub le)/cunion_countable=> i /=.
 case: (existsTP (fun s : seq T => {subset E i <= s}))=> /= [[s le_Eis]|].
   by apply/finite_countable/finiteP; exists s => x /le_Eis.
-move/finiteNP; pose j := `|floor (M / i.+1%:R)|.+1.
-pose K := (`|floor M|.+1 * i.+1)%N; move/(_ K)/asboolP/exists_asboolP.
-move=> h; have /asboolP[] := xchooseP h.
+move=> /finiteNP/(_ ((Num.trunc M).+1 * i.+1)%N)/asboolP/exists_asboolP h.
+have/asboolP[] := xchooseP h.
 set s := xchoose h=> eq_si uq_s le_sEi; pose J := [fset x in s].
 suff: \sum_(x : J) `|f (val x)| > M by rewrite ltNge bM.
 apply/(@lt_le_trans _ _ (\sum_(x : J) 1 / i.+1%:~R)); last first.
   apply/ler_sum=> /= m _; apply/ltW.
   by have:= fsvalP m; rewrite in_fset => /le_sEi.
-rewrite sumr_const -cardfE card_fseq undup_id // eq_si -mulr_natr -pmulrn.
-rewrite mul1r natrM mulrCA mulVf ?mulr1 ?pnatr_eq0 //.
-have /andP[_] := mem_rg1_Rfloor M; rewrite RfloorE -addn1.
-by rewrite natrD /= mulr1n pmulrn -{1}[floor _]gez0_abs // floor_ge0.
+rewrite mul1r sumr_const -cardfE card_fseq undup_id // eq_si.
+rewrite -mulr_natr natrM mulrC mulfK ?pnatr_eq0//.
+by case/trunc_itv/andP: ge0_M.
 Qed.
+
 End SummableCountable.
 
 (* -------------------------------------------------------------------- *)
@@ -1201,9 +1197,8 @@ Qed.
 
 Lemma sum_seq1 S x : (forall y, S y != 0 -> x == y) -> sum S = S x.
 Proof.
-move=> domS; rewrite (sum_finseq (r := [:: x])) //.
-  by move=> y; rewrite !inE => /domS /eqP->.
-by rewrite big_seq1.
+move=> domS; rewrite (sum_finseq (r := [:: x])) ?big_seq1//.
+by move=> y; rewrite !inE => /domS /eqP->.
 Qed.
 
 End SumTheory.
diff --git a/theories/ereal.v b/theories/ereal.v
index 4d2fcce6f..414423e22 100644
--- a/theories/ereal.v
+++ b/theories/ereal.v
@@ -5,8 +5,8 @@
 (* Copyright (c) - 2016--2018 - Polytechnique                           *)
 (* -------------------------------------------------------------------- *)
 From HB Require Import structures.
-From mathcomp Require Import all_ssreflect all_algebra finmap archimedean.
-From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
+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.
 Require Import reals signed topology.
 Require Export constructive_ereal.
@@ -55,6 +55,7 @@ Unset Printing Implicit Defensive.
 
 Import Order.TTheory GRing.Theory Num.Theory.
 Import numFieldTopology.Exports.
+From mathcomp Require Import mathcomp_extra.
 
 Local Open Scope ring_scope.
 
@@ -1266,7 +1267,7 @@ rewrite predeq2E => x A; split.
     case=> [r' /= re'r'| |]/=.
     * rewrite /ereal_ball in re'r'.
       have [r'r|rr'] := lerP (contract r'%:E) (contract r%:E).
-        apply: reA; rewrite /ball /= real_ltr_norml // ?num_real //.
+        apply: reA; rewrite /ball /= ltr_norml//.
         rewrite ger0_norm ?subr_ge0// in re'r'.
         have : (contract (r%:E - e%:num%:E) < contract r'%:E)%R.
           move: re'r'; rewrite /e' lt_min => /andP[+ _].
@@ -1276,7 +1277,7 @@ rewrite predeq2E => x A; split.
         rewrite ltrBlDr addrC -ltrBlDr => ->; rewrite andbT.
         rewrite (@lt_le_trans _ _ 0%R)// 1?ltrNl 1?oppr0// subr_ge0.
         by rewrite -lee_fin -le_contract.
-      apply: reA; rewrite /ball /= real_ltr_norml // ?num_real //.
+      apply: reA; rewrite /ball /= ltr_norml//.
       rewrite ltr0_norm ?subr_lt0// opprB in re'r'.
       apply/andP; split; last first.
         by rewrite (@lt_trans _ _ 0%R) // subr_lt0 -lte_fin -lt_contract.
@@ -1402,21 +1403,23 @@ Lemma cvg_ereal_loc_seq (R : realType) (x : \bar R) :
 Proof.
 move=> P; rewrite /ereal_loc_seq.
 case: x => /= [x [_/posnumP[d] dP] |[d [dreal dP]] |[d [dreal dP]]]; last 2 first.
-    have /ZnatP[N Nfloor] : floor (Num.max d 0%R) \is a Znat.
+    have /natrP[N Nfloor] : Num.floor (Num.max d 0%R) \is a Num.nat.
       by rewrite Znat_def floor_ge0 le_max lexx orbC.
     exists N.+1 => // n ltNn; apply: dP; rewrite lte_fin.
     have /le_lt_trans : (d <= Num.max d 0)%R by rewrite le_max lexx.
-    by apply; rewrite (lt_le_trans (reals.lt_succ_floor _))// Nfloor natr1 ler_nat.
-  have /ZnatP [N Nfloor] : floor (Num.max (- d)%R 0%R) \is a Znat.
+    apply; rewrite (lt_le_trans (lt_succ_floor _))// Nfloor.
+    by rewrite natr1 mulrz_nat ler_nat.
+  have /natrP[N Nfloor] : Num.floor (Num.max (- d)%R 0%R) \is a Num.nat.
     by rewrite Znat_def floor_ge0 le_max lexx orbC.
   exists N.+1 => // n ltNn; apply: dP; rewrite lte_fin ltrNl.
   have /le_lt_trans : (- d <= Num.max (- d) 0)%R by rewrite le_max lexx.
-  by apply; rewrite (lt_le_trans (reals.lt_succ_floor _))// Nfloor natr1 ler_nat.
-have /ZnatP[N Nfloor] : floor (d%:num^-1) \is a Num.nat.
+  apply; rewrite (lt_le_trans (lt_succ_floor _))// Nfloor.
+  by rewrite natr1 mulrz_nat ler_nat.
+have /natrP[N Nfloor] : Num.floor d%:num^-1 \is a Num.nat.
   by rewrite Znat_def floor_ge0.
 exists N => // n leNn; apply: dP; last first.
   by rewrite eq_sym addrC -subr_eq subrr eq_sym; exact/invr_neq0/lt0r_neq0.
 rewrite /= opprD addrA subrr distrC subr0 gtr0_norm; last by rewrite invr_gt0.
 rewrite -[ltLHS]mulr1 ltr_pdivrMl // -ltr_pdivrMr // div1r.
-by rewrite (lt_le_trans (reals.lt_succ_floor _))// Nfloor lerD// ler_nat.
+by rewrite (lt_le_trans (lt_succ_floor _))// Nfloor !natr1 mulrz_nat ler_nat.
 Qed.
diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v
index 16910f726..4daa6e2f6 100644
--- a/theories/lebesgue_integral.v
+++ b/theories/lebesgue_integral.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 archimedean.
-From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
+From mathcomp Require Import boolp classical_sets functions.
 From mathcomp Require Import cardinality fsbigop.
 Require Import signed reals ereal topology normedtype sequences real_interval.
 Require Import esum measure lebesgue_measure numfun realfun function_spaces.
@@ -83,6 +83,7 @@ Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 Import Order.TTheory GRing.Theory Num.Def Num.Theory.
 Import numFieldTopology.Exports.
+From mathcomp Require Import mathcomp_extra.
 
 Local Open Scope classical_set_scope.
 Local Open Scope ring_scope.
@@ -1286,28 +1287,20 @@ Qed.
 Lemma bigsetU_dyadic_itv n : `[n%:R, n.+1%:R[%classic =
   \big[setU/set0]_(n * 2 ^ n.+1 <= k < n.+1 * 2 ^ n.+1) [set` I n.+1 k].
 Proof.
-rewrite predeqE => r; split => [/= /[!in_itv]/= /andP[nr rn1]|].
-- rewrite -bigcup_seq /=; exists `|reals.floor (r * 2 ^+ n.+1)|%N.
-    rewrite /= mem_index_iota; apply/andP; split.
-      rewrite -ltez_nat gez0_abs ?reals.floor_ge0; last first.
-        by rewrite mulr_ge0// (le_trans _ nr).
-      apply: (@le_trans _ _ (reals.floor (n * 2 ^ n.+1)%:R)); last first.
-        by apply: le_floor; rewrite natrM natrX ler_pM2r.
-      by rewrite floor_natz intz.
-    rewrite -ltz_nat gez0_abs; last first.
-      by rewrite floor_ge0 mulr_ge0// (le_trans _ nr).
-    rewrite -(@ltr_int R) (le_lt_trans (reals.floor_le _))//.
-    by rewrite PoszM intrM -natrX ltr_pM2r.
-  rewrite /= in_itv /=; apply/andP; split.
-    rewrite ler_pdivrMr// (le_trans _ (reals.floor_le _))//.
-    by rewrite -(@gez0_abs (reals.floor _))// floor_ge0 mulr_ge0// (le_trans _ nr).
-  rewrite ltr_pdivlMr// (lt_le_trans (reals.lt_succ_floor _))//.
-  rewrite -[in leRHS]natr1 lerD2r// -(@gez0_abs (reals.floor _))// floor_ge0.
-  by rewrite mulr_ge0// (le_trans _ nr).
-- rewrite -bigcup_seq => -[/= k] /[!mem_index_iota] /andP[nk kn].
-  rewrite in_itv /= => /andP[knr rkn]; rewrite in_itv /=; apply/andP; split.
+rewrite predeqE => r; split => [/= /[!in_itv]/= /andP[nr rn1]|]; last first.
+  rewrite -bigcup_seq => -[/= k] /[!mem_index_iota] /andP[nk kn].
+  rewrite !in_itv /= => /andP[knr rkn]; apply/andP; split.
     by rewrite (le_trans _ knr)// ler_pdivlMr// -natrX -natrM ler_nat.
   by rewrite (lt_le_trans rkn)// ler_pdivrMr// -natrX -natrM ler_nat.
+rewrite -bigcup_seq /=; exists `|floor (r * 2 ^+ n.+1)|%N.
+  rewrite /= mem_index_iota -ltz_nat -lez_nat gez0_abs; last first.
+    by rewrite floor_ge0 mulr_ge0// (le_trans _ nr).
+  rewrite -floor_ge_int -floor_lt_int.
+  by rewrite !PoszM -!natrXE !rmorphM !rmorphXn /= ler_wpM2r ?ltr_pM2r.
+rewrite /= in_itv /= ler_pdivrMr// ltr_pdivlMr//.
+rewrite pmulrn [(`|_|.+1%:R)]pmulrn intS addrC gez0_abs; last first.
+  by rewrite floor_ge0 mulr_ge0 ?exprn_ge0 // (le_trans _ nr).
+by rewrite ge_floor lt_succ_floor.
 Qed.
 
 Lemma dyadic_itv_image n T (f : T -> \bar R) x :
@@ -1430,18 +1423,19 @@ rewrite pnatr_eq0 => /eqP.
 have [//|] := boolP (x \in B n).
 rewrite notin_setE /B /setI /= => /not_andP[] // /negP.
 rewrite -ltNge => fxn _.
-have K : (`|reals.floor (fine (f x) * 2 ^+ n)| < n * 2 ^ n)%N.
-  rewrite -ltz_nat gez0_abs; last by rewrite reals.floor_ge0 mulr_ge0// ltW.
-  rewrite -(@ltr_int R); rewrite (le_lt_trans (reals.floor_le _))// PoszM intrM.
+have K : (`|floor (fine (f x) * 2 ^+ n)| < n * 2 ^ n)%N.
+  rewrite -ltz_nat gez0_abs; last by rewrite floor_ge0 mulr_ge0// ltW.
+  rewrite -(@ltr_int R); rewrite (le_lt_trans (ge_floor _))// PoszM intrM.
   by rewrite -natrX ltr_pM2r// -lte_fin (fineK fxfin).
 have /[!mem_index_enum]/(_ isT) := An0 (Ordinal K).
 rewrite implyTb indicE mem_set ?mulr1; last first.
   rewrite /A K /= inE; split=> //=; exists (fine (f x)); last by rewrite fineK.
   rewrite in_itv /=; apply/andP; split.
-    rewrite ler_pdivrMr// (le_trans _ (reals.floor_le _))//.
-    by rewrite -(@gez0_abs (reals.floor _))// reals.floor_ge0 mulr_ge0// ltW.
-  rewrite ltr_pdivlMr// (lt_le_trans (reals.lt_succ_floor _))// -[in leRHS]natr1.
-  by rewrite lerD2r// -{1}(@gez0_abs (reals.floor _))// reals.floor_ge0// mulr_ge0// ltW.
+    rewrite ler_pdivrMr// (le_trans _ (ge_floor _))//.
+    by rewrite -(@gez0_abs (floor _))// floor_ge0 mulr_ge0// ltW.
+  rewrite ltr_pdivlMr// (lt_le_trans (lt_succ_floor _))//.
+  rewrite -[in leRHS]natr1 -intrD1 lerD2r// -{1}(@gez0_abs (floor _))//.
+  by rewrite floor_ge0// mulr_ge0// ltW.
 rewrite mulf_eq0// -exprVn; apply/negP; rewrite negb_or expf_neq0//= andbT.
 rewrite pnatr_eq0 -lt0n absz_gt0 floor_neq0// -ler_pdivrMr//.
 apply/orP; right; apply/ltW; near: n.
@@ -1538,11 +1532,11 @@ near=> n.
 have mn : (m <= n)%N by near: n; exists m.
 have : fine (f x) < n%:R.
   near: n.
-  exists `|reals.floor (fine (f x))|.+1%N => //= p /=.
+  exists `|floor (fine (f x))|.+1%N => //= p /=.
   rewrite -(@ler_nat R); apply: lt_le_trans.
-  rewrite -natr1 (_ : `| _ |%:R  = (reals.floor (fine (f x)))%:~R); last first.
-    by rewrite -[in RHS](@gez0_abs (reals.floor _))// reals.floor_ge0//; exact/fine_ge0/f0.
-  by rewrite reals.lt_succ_floor.
+  rewrite -natr1 (_ : `| _ |%:R  = (floor (fine (f x)))%:~R); last first.
+    by rewrite -[in RHS](@gez0_abs (floor _))// floor_ge0//; exact/fine_ge0/f0.
+  by rewrite intrD1 lt_succ_floor.
 rewrite -lte_fin (fineK fxfin) => fxn.
 have [approx_nx0|[k [/andP[k0 kn2n] ? ->]]] := f_ub_approx fxn.
   by have := Hm _ mn; rewrite approx_nx0.
@@ -1578,21 +1572,19 @@ move=> Dx fxoo; have approx_x n : approx n x = n%:R.
   by rewrite fgen_A0 // ?mulr0 // fxoo leey.
 case/cvg_ex => /= l; have [l0|l0] := leP 0%R l.
 - move=> /cvgrPdist_lt/(_ _ ltr01) -[n _].
-  move=> /(_ (`|reals.ceil l|.+1 + n)%N) /= /(_ (leq_addl _ _)).
+  move=> /(_ (`|ceil l|.+1 + n)%N) /= /(_ (leq_addl _ _)).
   rewrite approx_x.
   apply/negP; rewrite -leNgt distrC (le_trans _ (lerB_normD _ _)) //.
   rewrite normrN lerBrDl addSnnS [leRHS]ger0_norm ?ler0n//.
   rewrite natrD lerD// ?ler1n// ger0_norm // (le_trans (ceil_ge _)) //.
-  by rewrite -(@gez0_abs (reals.ceil _)) // ceil_ge0.
-- move/cvgrPdist_lt => /(_ _ ltr01) -[n _].
-  move=> /(_ (`|reals.floor l|.+1 + n)%N) /= /(_ (leq_addl _ _)).
-  rewrite approx_x.
-  apply/negP; rewrite -leNgt distrC (le_trans _ (lerB_normD _ _)) //.
+  by rewrite -(@gez0_abs (ceil _)) // -ceil_ge0 (lt_le_trans _ l0).
+- move=> /cvgrPdist_lt/(_ _ ltr01)[n _].
+  move=> /(_ (`|floor l|.+1 + n)%N)/(_ (leq_addl _ _)); apply/negP.
+  rewrite approx_x -leNgt distrC (le_trans _ (lerB_normD _ _))//.
   rewrite normrN lerBrDl addSnnS [leRHS]ger0_norm ?ler0n//.
-  rewrite natrD lerD// ?ler1n// ler0_norm //; last by rewrite ltW.
-  rewrite (@le_trans _ _ (- reals.floor l)%:~R) //.
-    by rewrite mulrNz lerNl opprK reals.floor_le.
-  by rewrite -(@lez0_abs (reals.floor _)) // reals.floor_le0 // ltW.
+  rewrite natrD lerD ?ler1n// ltr0_norm// (@le_trans _ _ (- floor l)%:~R)//.
+    by rewrite mulrNz lerNl opprK ge_floor.
+  by rewrite -(@lez0_abs (floor _))// -floor_le0// (lt_le_trans l0).
 Qed.
 
 Lemma ecvg_approx (f0 : forall x, D x -> (0 <= f x)%E) x :
@@ -2346,19 +2338,20 @@ transitivity (\int[mu]_(x in D) limn (g^~ x)).
       exists 1%N => // m /= m0.
       by rewrite mulry gtr0_sg// ?mul1e ?leey// ltr0n.
     near=> n; rewrite lee_fin -ler_pdivrMr//.
-    near: n; exists `|reals.ceil (M / r)|%N => // m /=.
+    near: n; exists `|ceil (M / r)|%N => // m /=.
     rewrite -(ler_nat R); apply: le_trans.
-    by rewrite natr_absz ger0_norm ?ceil_ge// ceil_ge0// divr_ge0// ?ltW.
+    rewrite natr_absz ger0_norm ?ceil_ge// -ceil_ge0// (lt_le_trans (ltrN10 _))//.
+    by rewrite divr_ge0// ?ltW.
   - rewrite lt0_mulye//; apply/cvgeNyPleNy; near=> M;
     have M0 : (M <= 0)%R by [].
     rewrite /g; case: (f x) fx0 => [r r0|//|_]; last first.
       exists 1%N => // m /= m0.
       by rewrite mulrNy gtr0_sg// ?ltr0n// mul1e ?leNye.
     near=> n; rewrite lee_fin -ler_ndivrMr//.
-    near: n; exists `|reals.ceil (M / r)|%N => // m /=.
+    near: n; exists `|ceil (M / r)|%N => // m /=.
     rewrite -(ler_nat R); apply: le_trans.
-    rewrite natr_absz ger0_norm ?ceil_ge// ceil_ge0// -mulrNN.
-    by rewrite mulr_ge0// lerNr oppr0// ltW// invr_lt0.
+    rewrite natr_absz ger0_norm ?ceil_ge// -ceil_ge0// (lt_le_trans (ltrN10 _))//.
+    by rewrite -mulrNN mulr_ge0// lerNr oppr0// ltW// invr_lt0.
   - rewrite -fx0 mule0 /g -fx0.
     under eq_fun do rewrite mule0/=. (*TODO: notation broken*)
     exact: cvg_cst.
@@ -2377,9 +2370,10 @@ rewrite -(@fineK _ (\int[mu]_(x in D) f x)); last first.
 rewrite -lee_pdivrMr//; last first.
   by move: if_gt0 ifoo; case: (\int[mu]_(x in D) f x).
 near: n.
-exists `|reals.ceil (M * (fine (\int[mu]_(x in D) f x))^-1)|%N => //.
+exists `|ceil (M * (fine (\int[mu]_(x in D) f x))^-1)|%N => //.
 move=> n /=; rewrite -(@ler_nat R) -lee_fin; apply: le_trans.
-rewrite lee_fin natr_absz ger0_norm ?ceil_ge// ceil_ge0//.
+rewrite lee_fin natr_absz ger0_norm ?ceil_ge// -ceil_ge0//.
+rewrite (lt_le_trans (ltrN10 _))//.
 by rewrite mulr_ge0// ?invr_ge0//; exact/fine_ge0/integral_ge0.
 Unshelve. all: by end_near. Qed.
 
@@ -2608,7 +2602,7 @@ Proof.
 move=> muD0; pose g : (T -> \bar R)^nat := fun n => cst n%:R%:E.
 have <- : (fun t => limn (g^~ t)) = cst +oo.
   rewrite funeqE => t; apply/cvg_lim => //=.
-  apply/cvgeryP/cvgryPge => M; exists `|reals.ceil M|%N => //= m.
+  apply/cvgeryP/cvgryPge => M; exists `|ceil M|%N => //= m.
   rewrite /= -(ler_nat R); apply: le_trans.
   by rewrite (le_trans (ceil_ge _))// natr_absz ler_int ler_norm.
 rewrite monotone_convergence //.
@@ -2617,7 +2611,7 @@ rewrite monotone_convergence //.
   have [muDoo|muDoo] := ltP (mu D) +oo; last first.
     exists 1%N => // m /= m0; move: muDoo; rewrite leye_eq => /eqP ->.
     by rewrite mulry gtr0_sg ?mul1e ?leey// ltr0n.
-  exists `|reals.ceil (M / fine (mu D))|%N => // m /=.
+  exists `|ceil (M / fine (mu D))|%N => // m /=.
   rewrite -(ler_nat R) => MDm; rewrite -(@fineK _ (mu D)) ?ge0_fin_numE//.
   rewrite -lee_pdivrMr; last by rewrite fine_gt0// lt0e muD0 measure_ge0.
   rewrite lee_fin (le_trans _ MDm)//.
@@ -3438,14 +3432,14 @@ have [M M0 muM] : exists2 M, (0 <= M)%R &
 apply/eqP/negPn/negP => /eqP muED0; move/not_forallP : muM; apply.
 have [muEDoo|] := ltP (mu (E `&` D)) +oo; last first.
   by rewrite leye_eq => /eqP ->; exists 1%N; rewrite mul1e leye_eq.
-exists `|reals.ceil (M * (fine (mu (E `&` D)))^-1)|%N.+1.
+exists `|ceil (M * (fine (mu (E `&` D)))^-1)|%N.+1.
 apply/negP; rewrite -ltNge.
 rewrite -[X in _ * X](@fineK _ (mu (E `&` D))); last first.
   by rewrite fin_numElt muEDoo (lt_le_trans _ (measure_ge0 _ _)).
 rewrite lte_fin -ltr_pdivrMr.
   rewrite -natr1 natr_absz ger0_norm.
     by rewrite (le_lt_trans (ceil_ge _))// ltrDl.
-  by rewrite ceil_ge0// divr_ge0//; apply/le0R/measure_ge0; exact: measurableI.
+  by rewrite -ceil_ge0// (lt_le_trans (ltrN10 _))// divr_ge0.
 rewrite -lte_fin fineK.
   rewrite lt0e measure_ge0 andbT.
   suff: E `&` D = E by move=> ->; exact/eqP.
@@ -3686,14 +3680,15 @@ move=> mf; split=> [iDf0|Df0].
     rewrite predeqE => t; split=> [[Dt ft0]|[n _ /= [Dt nft]]].
       have [ftoo|ftoo] := eqVneq `|f t| +oo.
         by exists 0%N => //; split => //=; rewrite ftoo /= leey.
-      pose m := `|reals.ceil (fine `|f t|)^-1|%N.
+      pose m := `|ceil (fine `|f t|)^-1|%N.
       have ftfin : `|f t|%E \is a fin_num by rewrite ge0_fin_numE// ltey.
       exists m => //; split => //=.
       rewrite -(@fineK _ `|f t|) // lee_fin -ler_pV2; last 2 first.
         - rewrite inE unitfE fine_eq0// abse_eq0 ft0/= fine_gt0//.
           by rewrite lt0e abse_ge0 abse_eq0 ft0 ltey.
         - by rewrite inE unitfE invr_eq0 pnatr_eq0 /= invr_gt0.
-      rewrite invrK /m -natr1 natr_absz ger0_norm ?ceil_ge0//.
+      rewrite invrK /m -natr1 natr_absz ger0_norm; last first.
+        by rewrite -ceil_ge0// (lt_le_trans (ltrN10 _)).
       rewrite (@le_trans _ _ ((fine `|f t|)^-1 + 1)%R) ?lerDl//.
       by rewrite lerD2r// ceil_ge.
     by split => //; apply: contraTN nft => /eqP ->; rewrite abse0 -ltNge.
@@ -6456,7 +6451,7 @@ move=> Ef; have {Ef} : mu.-negligible (E `&` [set x | 0 < f^* x]).
   near \oo => m; exists m => //=.
   rewrite -(@fineK _ (f^* x)) ?gt0_fin_numE ?ltey// lte_fin.
   rewrite invf_plt ?posrE//; last by rewrite fine_gt0// ltey fx0.
-  set r := _^-1; rewrite (@le_lt_trans _ _ `|reals.ceil r|.+1%:R)//.
+  set r := _^-1; rewrite (@le_lt_trans _ _ `|ceil r|.+1%:R)//.
     by rewrite (le_trans _ (abs_ceil_ge _))// ler_norm.
   by rewrite ltr_nat ltnS; near: m; exact: nbhs_infty_gt.
 apply: negligibleS => z /= /not_implyP[Ez H]; split => //.
@@ -6658,14 +6653,14 @@ have fE y k r : (ball 0%R k.+1%:R) y -> (r < 1)%R ->
   rewrite (le_trans (ltW yk1))// -lerBlDr opprK -lerBrDl.
   rewrite -natrB//; last by rewrite -addnn addSnnS ltn_addl.
   by rewrite -addnn addnK ler1n.
-have := h `|reals.ceil x|.+1%N Logic.I.
-have Bxx : B `|reals.ceil x|.+1 x.
+have := h `|ceil x|.+1%N Logic.I.
+have Bxx : B `|ceil x|.+1 x.
   rewrite /B /ball/= sub0r normrN (le_lt_trans (abs_ceil_ge _))// ltr_nat.
   by rewrite -addnn addSnnS ltn_addl.
 move=> /(_ Bxx)/fine_cvgP[davg_fk_fin_num davg_fk0].
 have f_fk_ceil : \forall t \near 0^'+,
   \int[mu]_(y in ball x t) `|(f y)%:E - (f x)%:E| =
-  \int[mu]_(y in ball x t) `|fk `|reals.ceil x|.+1 y - fk `|reals.ceil x|.+1 x|%:E.
+  \int[mu]_(y in ball x t) `|fk `|ceil x|.+1 y - fk `|ceil x|.+1 x|%:E.
   near=> t.
   apply: eq_integral => /= y /[1!inE] xty.
   rewrite -(fE x _ t)//; last first.
diff --git a/theories/lebesgue_measure.v b/theories/lebesgue_measure.v
index 3a85507b3..2190aa44c 100644
--- a/theories/lebesgue_measure.v
+++ b/theories/lebesgue_measure.v
@@ -1,6 +1,6 @@
 (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
 From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval.
-From mathcomp Require Import finmap fingroup perm rat.
+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.
 Require Import reals ereal signed topology numfun normedtype function_spaces.
@@ -1157,10 +1157,12 @@ rewrite predeqE => t; split => [/= [Dt ft]|].
   have [ft0|ft0] := leP 0%R (fine (f t)).
     exists `|ceil (fine (f t))|%N => //=; split => //; split.
       by rewrite -{2}(fineK ft)// lee_fin (le_trans _ ft0)// lerNl oppr0.
-    by rewrite natr_absz ger0_norm ?ceil_ge0// -(fineK ft) lee_fin ceil_ge.
+    rewrite natr_absz ger0_norm; last first.
+      by rewrite -ceil_ge0 (lt_le_trans _ ft0).
+    by rewrite -(fineK ft) lee_fin ceil_ge.
   exists `|floor (fine (f t))|%N => //=; split => //; split.
-    rewrite natr_absz ltr0_norm ?floor_lt0// EFinN.
-    by rewrite -{2}(fineK ft) lee_fin mulrNz opprK floor_le.
+    rewrite natr_absz ltr0_norm -?floor_lt0// EFinN.
+    by rewrite -{2}(fineK ft) lee_fin mulrNz opprK ge_floor// ?num_real.
   by rewrite -(fineK ft)// lee_fin (le_trans (ltW ft0)).
 move=> [n _] [/= Dt [nft fnt]]; split => //; rewrite fin_numElt.
 by rewrite (lt_le_trans _ nft) ?ltNyr//= (le_lt_trans fnt)// ltry.
@@ -1407,8 +1409,8 @@ move=> /(_ `|floor r|%N Logic.I); rewrite /= in_itv/= ltNge.
 rewrite lee_fin; have [r0|r0] := leP 0%R r.
   by rewrite (le_trans _ r0) // lerNl oppr0 ler0n.
 rewrite lerNl -abszN natr_absz gtr0_norm; last first.
-  by rewrite ltrNr oppr0 floor_lt0.
-by rewrite mulrNz lerNl opprK floor_le.
+  by rewrite ltrNr oppr0 -floor_lt0.
+by rewrite mulrNz lerNl opprK ge_floor.
 Qed.
 
 Lemma eset1y : [set +oo] = \bigcap_k `]k%:R%:E, +oo[%classic :> set (\bar R).
@@ -1417,7 +1419,7 @@ rewrite eqEsubset; split=> [_ -> i _/=|]; first by rewrite in_itv /= ltry.
 move=> [r| |/(_ O Logic.I)] // /(_ `|ceil r|%N Logic.I); rewrite /= in_itv /=.
 rewrite andbT lte_fin ltNge.
 have [r0|r0] := ltP 0%R r; last by rewrite (le_trans r0).
-by rewrite natr_absz gtr0_norm // ?ceil_ge// ceil_gt0.
+by rewrite natr_absz gtr0_norm// ?ceil_ge// -ceil_gt0.
 Qed.
 
 End erealwithrays.
@@ -2440,8 +2442,9 @@ have finite_set_F i : finite_set (F i).
     - by move=> /= x [n Fni Bnx]; exists n => //; exists i.
   have {CFi Fir2} := le_trans MC (le_trans CFi Fir2).
   apply/negP; rewrite -ltNge lebesgue_measure_ball// lte_fin.
-  rewrite -(@natr1 _ `| _ |%N) natr_absz ger0_norm ?ceil_ge0// -ltr_pdivrMr//.
-  by rewrite -ltrBlDr (lt_le_trans _ (ceil_ge _))// ltrBlDr ltrDl.
+  rewrite -(@natr1 _ `| _ |%N) natr_absz ger0_norm; last first.
+    by rewrite -ceil_ge0// (lt_le_trans (ltrN10 _)).
+  by rewrite -ltr_pdivrMr// -ltrBlDr (lt_le_trans _ (ceil_ge _))// ltrBlDr ltrDl.
 have mur2_fin_num_ : mu (ball (0:R) (r%:num + 2))%R < +oo.
   by rewrite lebesgue_measure_ball// ltry.
 have FE : \sum_(n <oo) \esum_(i in F n) mu (closure (B i)) =
diff --git a/theories/lebesgue_stieltjes_measure.v b/theories/lebesgue_stieltjes_measure.v
index f4c6d4217..a65d2e14c 100644
--- a/theories/lebesgue_stieltjes_measure.v
+++ b/theories/lebesgue_stieltjes_measure.v
@@ -1,6 +1,6 @@
 (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
 From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval.
-From mathcomp Require Import finmap fingroup perm rat.
+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.
@@ -482,12 +482,12 @@ Lemma wlength_sigma_finite (f : R -> R) :
 Proof.
 exists (fun k => `](- k%:R), k%:R]%classic).
   apply/esym; rewrite -subTset => /= x _ /=.
-  exists `|(floor `|x|%R + 1)%R|%N; rewrite //= in_itv/=.
-  rewrite !natr_absz intr_norm intrD -RfloorE.
-  suff: `|x| < `|Rfloor `|x| + 1| by rewrite ltr_norml => /andP[-> /ltW->].
+  exists `|(floor `|x| + 1)%R|%N; rewrite //= in_itv/=.
+  rewrite !natr_absz intr_norm intrD.
+  suff: `|x| < `|(floor `|x|)%:~R + 1| by rewrite ltr_norml => /andP[-> /ltW->].
   rewrite [ltRHS]ger0_norm//.
-    by rewrite (le_lt_trans _ (lt_succ_Rfloor _))// ?ler_norm.
-  by rewrite addr_ge0// -Rfloor0 le_Rfloor.
+    by rewrite intrD1 (le_lt_trans _ (lt_succ_floor _))// ?ler_norm.
+  by rewrite addr_ge0// ler0z floor_ge0.
 move=> k; split => //; rewrite wlength_itv /= -EFinB.
 by case: ifP; rewrite ltey.
 Qed.
diff --git a/theories/measure.v b/theories/measure.v
index 59f84235d..7bcba633e 100644
--- a/theories/measure.v
+++ b/theories/measure.v
@@ -1,5 +1,5 @@
 (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
-From mathcomp Require Import all_ssreflect all_algebra finmap.
+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.
 Require Import reals ereal signed topology normedtype sequences esum numfun.
@@ -2202,7 +2202,7 @@ Proof.
 move=> infA; apply/eqyP => r r0.
 have [B BA Br] := infinite_set_fset `|ceil r| infA.
 apply: esum_ge; exists [set` B] => //; apply: (@le_trans _ _ `|ceil r|%:R%:E).
-  by rewrite lee_fin natr_absz gtr0_norm ?ceil_gt0// ceil_ge.
+  by rewrite lee_fin natr_absz gtr0_norm -?ceil_gt0// ceil_ge.
 move: Br; rewrite -(@ler_nat R) -lee_fin => /le_trans; apply.
 rewrite (eq_fsbigr (cst 1))/=; last first.
   by move=> i /[!inE] /BA /mem_set iA; rewrite diracE iA.
@@ -2294,7 +2294,7 @@ move=> F mF tF mUF; rewrite [X in X @ \oo --> _](_ : _ =
     (fun n => (r%:num)%:E * \sum_(0 <= i < n) m (F i))); last first.
   by apply/funext => k; rewrite ge0_sume_distrr.
 rewrite /mscale; have [->|r0] := eqVneq r%:num 0%R.
-  rewrite mul0e [X in X @ \oo --> _](_ : _ = (fun=> 0)); first exact: cvg_cst.
+  rewrite mul0e [X in X @ \oo --> _](_ : _ = cst 0); first exact: cvg_cst.
   by under eq_fun do rewrite mul0e.
 by apply: cvgeMl => //; exact: measure_semi_sigma_additive.
 Qed.
diff --git a/theories/normedtype.v b/theories/normedtype.v
index 6b5b67271..721569595 100644
--- a/theories/normedtype.v
+++ b/theories/normedtype.v
@@ -2,7 +2,7 @@
 From HB Require Import structures.
 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 mathcomp_extra boolp classical_sets functions.
+From mathcomp Require Import boolp classical_sets functions.
 From mathcomp Require Import archimedean.
 From mathcomp Require Import cardinality set_interval Rstruct.
 Require Import ereal reals signed topology prodnormedzmodule function_spaces.
@@ -146,6 +146,7 @@ Unset Printing Implicit Defensive.
 
 Import Order.TTheory GRing.Theory Num.Def Num.Theory.
 Import numFieldTopology.Exports.
+From mathcomp Require Import mathcomp_extra.
 
 Local Open Scope classical_set_scope.
 Local Open Scope ring_scope.
@@ -252,13 +253,13 @@ End pseudoMetricnormedzmodule_lemmas.
 Lemma bigcup_ballT {R : realType} : \bigcup_n ball (0%R : R) n%:R = setT.
 Proof.
 apply/seteqP; split => // x _; have [x0|x0] := ltP 0%R x.
-  exists `|reals.ceil x|.+1 => //.
+  exists `|ceil x|.+1 => //.
   rewrite /ball /= sub0r normrN gtr0_norm// (le_lt_trans (ceil_ge _))//.
-  by rewrite -natr1 natr_absz -abszE gtz0_abs// ?ceil_gt0// ltr_pwDr.
-exists `|reals.ceil (- x)|.+1 => //.
+  by rewrite -natr1 natr_absz -abszE gtz0_abs// -?ceil_gt0// ltr_pwDr.
+exists `|ceil (- x)|.+1 => //.
 rewrite /ball /= sub0r normrN ler0_norm// (le_lt_trans (ceil_ge _))//.
-rewrite -natr1 natr_absz -abszE gez0_abs ?ceil_ge0// 1?lerNr ?oppr0//.
-by rewrite ltr_pwDr.
+rewrite -natr1 natr_absz -abszE gez0_abs ?ltr_pwDr// -ceil_ge0 ltrNl opprK.
+by rewrite (le_lt_trans x0).
 Qed.
 
 Section lower_semicontinuous.
@@ -596,8 +597,8 @@ Proof.
 split=> [/cvgryPge|/cvgnyPge] Foo.
   by apply/cvgnyPge => A; near do rewrite -(@ler_nat R); apply: Foo.
 apply/cvgryPgey; near=> A; near=> n.
-rewrite (le_trans (@ceil_ge R A))// (ler_int _ _ (f n)) [reals.ceil _]intEsign.
-by rewrite le_gtF ?expr0 ?mul1r ?lez_nat ?ceil_ge0//; near: n; apply: Foo.
+rewrite (le_trans (@ceil_ge R A))// (ler_int _ _ (f n)) [ceil _]intEsign.
+by rewrite le_gtF ?expr0 ?mul1r ?lez_nat -?ceil_ge0//; near: n; apply: Foo.
 Unshelve. all: by end_near. Qed.
 
 Section ecvg_infty_numField.
@@ -4919,7 +4920,7 @@ Lemma compact_bounded (K : realType) (V : normedModType K) (A : set V) :
 Proof.
 rewrite compact_cover => Aco.
 have covA : A `<=` \bigcup_(n : int) [set p | `|p| < n%:~R].
-  by move=> p _; exists (reals.floor `|p| + 1) => //; rewrite rmorphD/= reals.lt_succ_floor.
+  by move=> p _; exists (floor `|p| + 1) => //=; rewrite lt_succ_floor.
 have /Aco [] := covA.
   move=> n _; rewrite openE => p; rewrite /= -subr_gt0 => ltpn.
   apply/nbhs_ballP; exists (n%:~R - `|p|) => // q.
@@ -5763,13 +5764,13 @@ Notation r_gt0 := vitali_collection_partition_ub_gt0.
 Lemma ex_vitali_collection_partition i :
   V i -> exists n, vitali_collection_partition n i.
 Proof.
-move=> Vi; pose f := reals.floor (r / (radius (B i))%:num).
+move=> Vi; pose f := floor (r / (radius (B i))%:num).
 have f_ge0 : 0 <= f by rewrite floor_ge0// divr_ge0// ltW// (r_gt0 Vi).
 have [m /andP[mf fm]] := leq_ltn_expn `|f|.-1.
 exists m; split => //; apply/andP; split => [{mf}|{fm}].
   rewrite -(@ler_nat R) in fm.
   rewrite ltr_pdivrMr// mulrC -ltr_pdivrMr// (lt_le_trans _ fm)//.
-  rewrite (lt_le_trans (reals.lt_succ_floor _))//= -/f -natr1 lerD2r//.
+  rewrite (lt_le_trans (lt_succ_floor _))//= -/f intrD -natr1 lerD2r//.
   have [<-|f0] := eqVneq 0 f; first by rewrite /= ler0n.
   rewrite prednK//; last by rewrite absz_gt0 eq_sym.
   by rewrite natr_absz// ger0_norm.
@@ -5779,7 +5780,7 @@ rewrite ler_pdivlMr// mulrC -ler_pdivlMr//.
 have [f0|f0] := eqVneq 0 f.
   by move: mf; rewrite -f0 absz0 leNgt expnS ltr_nat leq_pmulr// expn_gt0.
 rewrite (le_trans mf)// prednK//; last by rewrite absz_gt0 eq_sym.
-by rewrite natr_absz// ger0_norm// reals.floor_le.
+by rewrite natr_absz// ger0_norm// ge_floor.
 Qed.
 
 Lemma cover_vitali_collection_partition :
@@ -5972,7 +5973,7 @@ exists j; split => //.
 Qed.
 
 Lemma vitali_lemma_infinite_cover : { D : set I | [/\ countable D,
-  D `<=` V, trivIset D (closure\o B) &
+  D `<=` V, trivIset D (closure \o B) &
   cover V (closure \o B) `<=` cover D (closure \o scale_ball 5%:R \o B)] }.
 Proof.
 have [D [cD DV tD maxD]] := vitali_lemma_infinite.
diff --git a/theories/real_interval.v b/theories/real_interval.v
index cc90e5e51..f9feec095 100644
--- a/theories/real_interval.v
+++ b/theories/real_interval.v
@@ -1,7 +1,7 @@
 (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
 From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval.
-From mathcomp Require Import finmap fingroup perm rat.
-From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
+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.
 Require Import reals ereal signed topology normedtype sequences.
@@ -14,6 +14,7 @@ Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 Import Order.TTheory GRing.Theory Num.Def Num.Theory.
+From mathcomp Require Import mathcomp_extra.
 
 Local Open Scope classical_set_scope.
 Local Open Scope ring_scope.
@@ -176,7 +177,7 @@ rewrite predeqE => y; split=> /=; last first.
 rewrite in_itv /= andbT => xy; exists `|floor y|%N.+1 => //=.
 rewrite in_itv /= xy /=.
 have [y0|y0] := ltP 0 y; last by rewrite (le_lt_trans y0)// ltr_pwDr.
-by rewrite -natr1 natr_absz ger0_norm ?floor_ge0 1?ltW// lt_succ_floor.
+by rewrite -natr1 natr_absz ger0_norm ?floor_ge0 1?ltW// intrD1 lt_succ_floor.
 Qed.
 
 Lemma itv_o_inftyEbigcup x :
@@ -340,10 +341,10 @@ move gxE : (g x) => gx; case: gx gxE => [gx| |gxoo fxoo]; last 2 first.
   - by exists 0%N => //; rewrite /E/= gxoo addey// ?leey// -ltNye.
 move fxE : (f x) => fx; case: fx fxE => [fx fxE gxE|fxoo gxE _|//]; last first.
   by exists 0%N => //; rewrite /E/= fxoo gxE// addye// leey.
-rewrite lte_fin -subr_gt0 => fgx; exists `|floor (fx - gx)^-1%R|%N => //.
+rewrite lte_fin -subr_gt0 => fgx; exists `|floor (fx - gx)^-1|%N => //.
 rewrite /E/= -natr1 natr_absz ger0_norm ?floor_ge0 ?invr_ge0; last exact/ltW.
 rewrite fxE gxE lee_fin -[leRHS]invrK lef_pV2//.
-- by apply/ltW; rewrite lt_succ_floor.
+- by rewrite intrD1 ltW// lt_succ_floor.
 - by rewrite posrE// ltr_pwDr// ler0z floor_ge0 invr_ge0 ltW.
 - by rewrite posrE invr_gt0.
 Qed.
@@ -363,9 +364,10 @@ apply/seteqP; split=> [x ->|].
   by move=> i _/=; rewrite in_itv/= lexx ltrBlDr ltrDl invr_gt0 ltr0n.
 move=> x rx; apply/esym/eqP; rewrite eq_le (itvP (rx 0%N _))// andbT.
 apply/ler_addgt0Pl => e e_gt0; rewrite -lerBlDl ltW//.
-have := rx `|floor e^-1%R|%N I; rewrite /= in_itv => /andP[/le_lt_trans->]//.
+have := rx `|floor e^-1|%N I; rewrite /= in_itv => /andP[/le_lt_trans->]//.
 rewrite lerD2l lerN2 -lef_pV2 ?invrK//; last by rewrite posrE.
-by rewrite -natr1 natr_absz ger0_norm ?floor_ge0 ?invr_ge0 1?ltW// lt_succ_floor.
+rewrite -natr1 natr_absz ger0_norm ?floor_ge0 ?invr_ge0 1?ltW//.
+by rewrite intrD1 lt_succ_floor.
 Qed.
 
 Lemma itv_bnd_open_bigcup (R : realType) b (r s : R) :
@@ -375,11 +377,11 @@ Proof.
 apply/seteqP; split => [x/=|]; last first.
   move=> x [n _ /=] /[!in_itv] /andP[-> /le_lt_trans]; apply.
   by rewrite ltrBlDr ltrDl invr_gt0 ltr0n.
-rewrite in_itv/= => /andP[sx xs]; exists `|ceil ((s - x)^-1)|%N => //=.
+rewrite in_itv/= => /andP[sx xs]; exists `|ceil (s - x)^-1|%N => //=.
 rewrite in_itv/= sx/= lerBrDl addrC -lerBrDl.
 rewrite -[in X in _ <= X](invrK (s - x)) ler_pV2.
 - rewrite -natr1 natr_absz ger0_norm; last first.
-    by rewrite ceil_ge0// invr_ge0 subr_ge0 ltW.
+    by rewrite -ceil_ge0 (lt_le_trans (ltrN10 R))// invr_ge0 subr_ge0 ltW.
   by rewrite (@le_trans _ _ (ceil (s - x)^-1)%:~R)// ?lerDl// ceil_ge.
 - by rewrite inE unitfE ltr0n andbT pnatr_eq0.
 - by rewrite inE invr_gt0 subr_gt0 xs andbT unitfE invr_eq0 subr_eq0 gt_eqF.
@@ -403,7 +405,8 @@ Proof.
 apply/seteqP; split=> y; rewrite /= !in_itv/= andbT; last first.
   by move=> [k _ /=]; move: b => [|] /=; rewrite in_itv/= => /andP[//] /ltW.
 move=> xy; exists `|ceil (y - x)|%N => //=; rewrite in_itv/= xy/= -lerBlDl.
-rewrite !natr_absz/= ger0_norm ?ceil_ge0 ?subr_ge0 ?ceil_ge//.
+rewrite !natr_absz/= ger0_norm -?ceil_ge0 ?ceil_ge//.
+rewrite (lt_le_trans (ltrN10 R))// subr_ge0.
 by case: b xy => //= /ltW.
 Qed.
 
@@ -424,7 +427,7 @@ Proof.
 rewrite -subTset => x _ /=; exists `|(floor `|x| + 1)%R|%N => //=.
 rewrite in_itv/= !natr_absz intr_norm intrD.
 have : `|x| < `|(floor `|x|)%:~R + 1|.
-  by rewrite [ltRHS]ger0_norm ?lt_succ_floor// addr_ge0// ler0z floor_ge0.
+  by rewrite [ltRHS]ger0_norm ?intrD1 ?lt_succ_floor// ler0z addr_ge0// floor_ge0.
 case: b => /=.
 - by move/ltW; rewrite ler_norml => /andP[-> ->].
 - by rewrite ltr_norml => /andP[-> /ltW->].
diff --git a/theories/realfun.v b/theories/realfun.v
index 1507cc6eb..24735d797 100644
--- a/theories/realfun.v
+++ b/theories/realfun.v
@@ -1,6 +1,7 @@
 (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
-From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum finmap.
+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.
 Require Import ereal reals signed topology prodnormedzmodule normedtype derive.
@@ -183,9 +184,9 @@ exists (fun n => sval (cid (He (PosNum (invn n))))).
   apply/cvgrPdist_lt => r r0; near=> t.
   rewrite /sval/=; case: cid => x [px xpt _].
   rewrite distrC (lt_le_trans xpt)// -(@invrK _ r) lef_pV2 ?posrE ?invr_gt0//.
-  near: t; exists `|ceil (r^-1)|%N => // s /=.
+  near: t; exists `|ceil r^-1|%N => // s /=.
   rewrite -ltnS -(@ltr_nat R) => /ltW; apply: le_trans.
-  by rewrite natr_absz gtr0_norm ?ceil_gt0 ?invr_gt0// ceil_ge.
+  by rewrite natr_absz gtr0_norm -?ceil_gt0 ?invr_gt0// ceil_ge.
 move=> /cvgrPdist_lt/(_ e%:num (ltac:(by [])))[] n _ /(_ _ (leqnn _)).
 rewrite /sval/=; case: cid => // x [px xpn].
 by rewrite leNgt distrC => /negP.
@@ -235,7 +236,7 @@ have y_p : y_ n @[n --> \oo] --> p.
   near: t.
   exists `|ceil e^-1|%N => // k /= ek.
   rewrite (le_trans (ceil_ge _))// (@le_trans _ _ `|ceil e^-1|%:~R)//.
-    by rewrite ger0_norm// ?ceil_ge0// ?invr_ge0// ltW.
+    by rewrite ger0_norm -?ceil_ge0// (lt_le_trans (ltrN10 _))// invr_ge0// ltW.
   by move: ek;rewrite -(leq_add2r 1) !addn1 -(ltr_nat R) => /ltW.
 have /fine_cvgP[[m _ mfy_] /= _] := h _ (conj py_ y_p).
 near \oo => n.
@@ -1426,7 +1427,6 @@ Proof. by move=> fct fK; have [] := near_can_continuousAcan_sym fK fct. Qed.
 End real_inverse_functions.
 
 Section real_inverse_function_instances.
-
 Variable R : realType.
 
 Lemma exprn_continuous n : continuous (@GRing.exp R ^~ n).
@@ -2268,7 +2268,7 @@ have Nffin : TV a x (\- f) \is a fin_num.
   exact: (bounded_variationl ax xb).
 rewrite /pos_tv /neg_tv /= total_variationN -fineB -?muleBl // ?fineM //.
 - rewrite addeAC oppeD //= ?fin_num_adde_defl //.
-  by rewrite addeA subee // add0e -EFinD //= opprK mulrDl -Num.Theory.splitr.
+  by rewrite addeA subee // add0e -EFinD //= opprK mulrDl -splitr.
 - by rewrite fin_numB ?fin_numD ?ffin; apply/andP; split.
 - by apply: fin_num_adde_defl; rewrite fin_numN fin_numD; apply/andP; split.
 - by rewrite fin_numM // fin_numD; apply/andP; split.
@@ -2343,7 +2343,7 @@ rewrite {1}variation_prev; last exact: itv_partition1.
 rewrite /= -addeA -lteBrDr; last by rewrite fin_numD; apply/andP.
 rewrite EFinD -lte_fin ?fineK // oppeD //= ?fin_num_adde_defl // opprK addeA.
 move/lt_trans; apply.
-rewrite [x in (_ < x%:E)%E]Num.Theory.splitr EFinD addeC lteD2lE //.
+rewrite [x in (_ < x%:E)%E]splitr EFinD addeC lteD2lE //.
 rewrite -addeA.
 apply: (@le_lt_trans _ _ (variation x t f (t :: nil))%:E).
   rewrite [in leRHS]variation_prev; last exact: itv_partition1.
diff --git a/theories/reals.v b/theories/reals.v
index cf231eb6e..1e41479c7 100644
--- a/theories/reals.v
+++ b/theories/reals.v
@@ -32,18 +32,15 @@
 (*     Rtoint r == r when r is an integer, 0 otherwise                        *)
 (*  floor_set x := [set y | Rtoint y /\ y <= x]                               *)
 (*     Rfloor x == the floor of x as a real number                            *)
-(*      floor x == the floor of x as an integer (type int)                    *)
 (*     range1 x := [set y |x <= y < x + 1]                                    *)
 (*      Rceil x == the ceil of x as a real number, i.e., - Rfloor (- x)       *)
-(*       ceil x := - floor (- x)                                              *)
 (* ```                                                                        *)
 (*                                                                            *)
 (******************************************************************************)
 
 From HB Require Import structures.
-From mathcomp Require Import all_ssreflect all_algebra.
-From mathcomp Require Import mathcomp_extra boolp classical_sets set_interval.
-From mathcomp Require Import archimedean.
+From mathcomp Require Import all_ssreflect all_algebra archimedean.
+From mathcomp Require Import boolp classical_sets set_interval.
 
 Require Import Setoid.
 
@@ -56,6 +53,7 @@ Unset Printing Implicit Defensive.
 Unset SsrOldRewriteGoalsOrder.
 
 Import Order.TTheory Order.Syntax GRing.Theory Num.Def Num.Theory.
+From mathcomp Require Import mathcomp_extra.
 
 (* -------------------------------------------------------------------- *)
 Delimit Scope real_scope with real.
@@ -97,9 +95,7 @@ Implicit Types x : R.
 Lemma has_ub_image_norm E : has_ubound (normr @` E) -> has_ubound E.
 Proof.
 case => M /ubP uM; exists `|M|; apply/ubP => r rS.
-rewrite (le_trans (real_ler_norm _)) ?num_real //.
-rewrite (le_trans (uM _ _)) ?real_ler_norm ?num_real //.
-by exists r.
+by rewrite (le_trans (ler_norm _))// (le_trans (uM _ _))//; exact: ler_norm.
 Qed.
 
 Lemma has_inf_supN E : has_sup (-%R @` E) <-> has_inf E.
@@ -121,12 +117,10 @@ End has_bound_lemmas.
 (* -------------------------------------------------------------------- *)
 
 HB.mixin Record ArchimedeanField_isReal R of Num.ArchiField R := {
-  sup_upper_bound_subdef :
-    forall E : set [the archiFieldType of R],
-      has_sup E -> ubound E (supremum 0 E) ;
-  sup_adherent_subdef :
-    forall (E : set [the archiFieldType of R]) (eps : R), 0 < eps ->
-      has_sup E -> exists2 e : R, E e & (supremum 0 E - eps) < e ;
+  sup_upper_bound_subdef : forall E : set [the archiFieldType of R],
+    has_sup E -> ubound E (supremum 0 E) ;
+  sup_adherent_subdef : forall (E : set [the archiFieldType of R]) (eps : R),
+    0 < eps -> has_sup E -> exists2 e : R, E e & (supremum 0 E - eps) < e
 }.
 
 #[short(type=realType)]
@@ -137,8 +131,6 @@ Bind Scope ring_scope with Real.sort.
 
 (* -------------------------------------------------------------------- *)
 Definition sup {R : realType} := @supremum _ R 0.
-(*Local Notation "-` E" := [pred x | - x \in E]
-  (at level 35, right associativity) : function_scope.*)
 Definition inf {R : realType} (E : set R) := - sup (-%R @` E).
 
 (* -------------------------------------------------------------------- *)
@@ -238,21 +230,18 @@ Qed.
 End ToInt.
 
 (* -------------------------------------------------------------------- *)
+
 Section RealDerivedOps.
 Variable R : realType.
 
 Implicit Types x y : R.
 Definition floor_set x := [set y : R | (y \is a Rint) && (y <= x)].
 
-Definition Rfloor x : R := sup (floor_set x).
-
-Definition floor x : int := Rtoint (Rfloor x).
+Definition Rfloor x : R := (floor x)%:~R.
 
 Definition range1 (x : R) := [set y | x <= y < x + 1].
 
-Definition Rceil x := - Rfloor (- x).
-
-Definition ceil x := - floor (- x).
+Definition Rceil x : R := (ceil x)%:~R.
 
 End RealDerivedOps.
 
@@ -340,14 +329,14 @@ have ABsup : has_sup [set x + y | x in A & y in B].
 apply: le_anti; apply/andP; split.
   apply: sup_le_ub; first by case: ABsup.
   by move=> ? [p Ap [q Bq] <-]; apply: lerD; exact: sup_ub.
-rewrite real_leNgt ?num_real// -subr_gt0; apply/negP.
+rewrite leNgt -subr_gt0; apply/negP.
 set eps := (_ + _ - _) => epos.
 have e2pos : 0 < eps / 2%:R by rewrite divr_gt0// ltr0n.
 have [r Ar supBr] := sup_adherent e2pos supA.
 have [s Bs supAs] := sup_adherent e2pos supB.
 have := ltrD supBr supAs.
 rewrite -addrA [-_+_]addrC -addrA -opprD -splitr addrA /= opprD opprK addrA.
-rewrite subrr add0r; apply/negP; rewrite -real_leNgt ?num_real//.
+rewrite subrr add0r; apply/negP; rewrite -leNgt.
 by apply: sup_upper_bound => //; exists r => //; exists s.
 Qed.
 
@@ -470,27 +459,23 @@ by rewrite absz_eq0 subr_eq0 eq_sym (negbTE ne_yz).
 Qed.
 
 Lemma isint_Rfloor x : Rfloor x \is a Rint.
-Proof. by case/andP: (sup_in_floor_set x). Qed.
+Proof. by rewrite inE; exists (floor x). Qed.
 
 Lemma RfloorE x : Rfloor x = (floor x)%:~R.
-Proof. by rewrite /floor RtointK ?isint_Rfloor. Qed.
+Proof. by []. Qed.
+
+Lemma mem_rg1_floor x : (range1 (floor x)%:~R) x.
+Proof. by rewrite /range1 /mkset intrD1 ge_floor lt_succ_floor. Qed.
 
 Lemma mem_rg1_Rfloor x : (range1 (Rfloor x)) x.
-Proof.
-rewrite /range1/mkset.
-have /andP[_ ->] /= := sup_in_floor_set x.
-have [|] := pselect ((floor_set x) (Rfloor x + 1)); last first.
-  rewrite /floor_set => /negP.
-  by rewrite negb_and -ltNge rpredD // ?(Rint1, isint_Rfloor).
-move/ubP : (sup_upper_bound (has_sup_floor_set x)) => h/h.
-by rewrite gerDl ler10.
-Qed.
+Proof. exact: mem_rg1_floor. Qed.
 
 Lemma Rfloor_le x : Rfloor x <= x.
 Proof. by case/andP: (mem_rg1_Rfloor x). Qed.
 
+#[deprecated(since="mathcomp-analysis 1.3.0", note="use `ge_floor` instead")]
 Lemma floor_le x : (floor x)%:~R <= x.
-Proof. by rewrite -RfloorE; exact: Rfloor_le. Qed.
+Proof. by rewrite ge_floor. Qed.
 
 Lemma lt_succ_Rfloor x : x < Rfloor x + 1.
 Proof. by case/andP: (mem_rg1_Rfloor x). Qed.
@@ -511,34 +496,24 @@ Proof. by rewrite /range1/mkset lexx /= ltrDl ltr01. Qed.
 Lemma range1zP (m : int) x : Rfloor x = m%:~R <-> (range1 m%:~R) x.
 Proof.
 split=> [<-|h]; first exact/mem_rg1_Rfloor.
-apply/eqP; rewrite RfloorE eqr_int; apply/eqP/(@range1z_inj x) => //.
-by rewrite /range1/mkset -RfloorE mem_rg1_Rfloor.
+by congr intmul; apply/floor_def; rewrite -intrD1.
 Qed.
 
 Lemma Rfloor_natz (z : int) : Rfloor z%:~R = z%:~R :> R.
 Proof. by apply/range1zP/range1rr. Qed.
 
-Lemma Rfloor0 : Rfloor 0 = 0 :> R.
-Proof. by rewrite -{1}(mulr0z 1) Rfloor_natz. Qed.
+Lemma Rfloor0 : Rfloor 0 = 0 :> R. Proof. by rewrite /Rfloor floor0. Qed.
 
-Lemma Rfloor1 : Rfloor 1 = 1 :> R.
-Proof. by rewrite -{1}(mulr1z 1) Rfloor_natz. Qed.
+Lemma Rfloor1 : Rfloor 1 = 1 :> R. Proof. by rewrite /Rfloor floor1. Qed.
 
 Lemma le_Rfloor : {homo (@Rfloor R) : x y / x <= y}.
-Proof.
-move=> x y le_xy; case: lerP=> //=; rewrite -Rint_ler_addr1 ?isint_Rfloor //.
-move/(lt_le_trans (lt_succ_Rfloor y))/lt_le_trans/(_ (Rfloor_le x)).
-by rewrite ltNge le_xy.
-Qed.
+Proof. by move=> x y /Num.Theory.floor_le; rewrite ler_int. Qed.
 
 Lemma Rfloor_ge_int x (n : int) : (n%:~R <= x)= (n%:~R <= Rfloor x).
-Proof.
-apply/idP/idP; last by move/le_trans => /(_ _ (Rfloor_le x)).
-by move/le_Rfloor; apply le_trans; rewrite Rfloor_natz.
-Qed.
+Proof. by rewrite ler_int floor_ge_int. Qed.
 
 Lemma Rfloor_lt_int x (z : int) : (x < z%:~R) = (Rfloor x < z%:~R).
-Proof. by rewrite ltNge Rfloor_ge_int -ltNge. Qed.
+Proof. by rewrite ltr_int floor_lt_int. Qed.
 
 Lemma Rfloor_le0 x : x <= 0 -> Rfloor x <= 0.
 Proof. by move=> ?; rewrite -Rfloor0 le_Rfloor. Qed.
@@ -546,44 +521,9 @@ Proof. by move=> ?; rewrite -Rfloor0 le_Rfloor. Qed.
 Lemma Rfloor_lt0 x : x < 0 -> Rfloor x < 0.
 Proof. by move=> x0; rewrite (le_lt_trans _ x0) // Rfloor_le. Qed.
 
-Lemma floor_natz n : floor (n%:R : R) = n%:~R :> int.
-Proof. by rewrite /floor (Rfloor_natz n) Rtointz intz. Qed.
-
-Lemma floor0 : floor (0 : R) = 0.
-Proof. by rewrite /floor Rfloor0 (_ : 0 = 0%:R) // Rtointn. Qed.
-
-Lemma floor1 : floor (1 : R) = 1.
-Proof. by rewrite /floor Rfloor1 (_ : 1 = 1%:R) // Rtointn. Qed.
-
-Lemma floor_ge0 x : (0 <= floor x) = (0 <= x).
-Proof. by rewrite -(@ler_int R) -RfloorE -Rfloor_ge_int. Qed.
-
-Lemma floor_le0 x : x <= 0 -> floor x <= 0.
-Proof. by move=> ?; rewrite -(@ler_int R) -RfloorE Rfloor_le0. Qed.
-
-Lemma floor_lt0 x : x < 0 -> floor x < 0.
-Proof. by move=> ?; rewrite -(@ltrz0 R) RtointK ?isint_Rfloor// Rfloor_lt0. Qed.
-
-Lemma le_floor : {homo @floor R : x y / x <= y}.
-Proof. by move=>*; rewrite -(@ler_int R) !RtointK ?isint_Rfloor ?le_Rfloor. Qed.
-
-Lemma floor_neq0 x : (floor x != 0) = (x < 0) || (x >= 1).
-Proof.
-apply/idP/orP => [|[x0|/le_floor r1]]; first rewrite neq_lt => /orP[x0|x0].
-- by left; apply: contra_lt x0; rewrite floor_ge0.
-- by right; rewrite (le_trans _ (floor_le _))// ler1z -gtz0_ge1.
-- by rewrite lt_eqF//; apply: contra_lt x0; rewrite floor_ge0.
-- by rewrite gt_eqF// (lt_le_trans _ r1)// floor1.
-Qed.
-
-Lemma lt_succ_floor x : x < (floor x)%:~R + 1.
-Proof. by rewrite -RfloorE lt_succ_Rfloor. Qed.
-
-Lemma floor_lt_int x (z : int) : (x < z%:~R) = (floor x < z).
-Proof. by rewrite Rfloor_lt_int RfloorE ltr_int. Qed.
-
-Lemma floor_ge_int x (z : int) : (z%:~R <= x) = (z <= floor x).
-Proof. by rewrite Rfloor_ge_int RfloorE ler_int. Qed.
+#[deprecated(since="mathcomp-analysis 1.3.0", note="use `Num.Theory.floor_le` instead")]
+Lemma le_floor : {homo @Num.floor R : x y / x <= y}.
+Proof. exact: Num.Theory.floor_le. Qed.
 
 Lemma ltr_add_invr (y x : R) : y < x -> exists k, y + k.+1%:R^-1 < x.
 Proof.
@@ -591,8 +531,8 @@ move=> yx; exists `|floor (x - y)^-1|%N.
 rewrite -ltrBrDl -{2}(invrK (x - y)%R) ltf_pV2 ?qualifE/= ?ltr0n//.
   by rewrite invr_gt0 subr_gt0.
 rewrite -natr1 natr_absz ger0_norm.
-  by rewrite floor_ge0 invr_ge0 subr_ge0 ltW.
-by rewrite -RfloorE lt_succ_Rfloor.
+  by rewrite -floor_ge_int// invr_ge0 subr_ge0 ltW.
+by rewrite intrD1 lt_succ_floor.
 Qed.
 
 End FloorTheory.
@@ -603,54 +543,26 @@ Variable R : realType.
 Implicit Types x y : R.
 
 Lemma isint_Rceil x : Rceil x \is a Rint.
-Proof. by rewrite /Rceil rpredN isint_Rfloor. Qed.
+Proof. by rewrite /Rceil RintC. Qed.
 
 Lemma Rceil0 : Rceil 0 = 0 :> R.
-Proof. by rewrite /Rceil oppr0 Rfloor0 oppr0. Qed.
+Proof. by rewrite /Rceil ceil0. Qed.
 
 Lemma Rceil_ge x : x <= Rceil x.
-Proof. by rewrite /Rceil lerNr Rfloor_le. Qed.
+Proof. by rewrite /Rceil le_ceil// num_real. Qed.
 
 Lemma le_Rceil : {homo (@Rceil R) : x y / x <= y}.
-Proof. by move=> x y ?; rewrite lerNl opprK le_Rfloor // lerNl opprK. Qed.
+Proof. by move=> x y ?; rewrite /Rceil ler_int ceil_le. Qed.
 
 Lemma Rceil_ge0 x : 0 <= x -> 0 <= Rceil x.
-Proof. by move=> ?; rewrite -Rceil0 le_Rceil. Qed.
+Proof. by move=> x0; rewrite /Rceil ler0z -(ceil0 R) ceil_le. Qed.
 
 Lemma RceilE x : Rceil x = (ceil x)%:~R.
-Proof. by rewrite /Rceil /ceil RfloorE mulrNz. Qed.
-
-Lemma ceil_ge x : x <= (ceil x)%:~R.
-Proof. by rewrite -RceilE; exact: Rceil_ge. Qed.
-
-Lemma ceil_ge0 x : 0 <= x -> 0 <= ceil x.
-Proof. by move/(ge_trans (ceil_ge x)); rewrite -(ler_int R). Qed.
-
-Lemma ceil_gt0 x : 0 < x -> 0 < ceil x.
-Proof. by move=> ?; rewrite /ceil oppr_gt0 floor_lt0 // ltrNl oppr0. Qed.
-
-Lemma ceil_le0 x : x <= 0 -> ceil x <= 0.
-Proof. by move=> x0; rewrite -lerNl oppr0 floor_ge0 -lerNr oppr0. Qed.
-
-Lemma le_ceil : {homo @ceil R : x y / x <= y}.
-Proof. by move=> x y xy; rewrite lerNl opprK le_floor // lerNl opprK. Qed.
-
-Lemma ceil_ge_int x (z : int) : (x <= z%:~R) = (ceil x <= z).
-Proof. by rewrite /ceil lerNl -floor_ge_int// -lerNr mulrNz opprK. Qed.
-
-Lemma ceil_lt_int x (z : int) : (z%:~R < x) = (z < ceil x).
-Proof. by rewrite ltNge ceil_ge_int -ltNge. Qed.
-
-Lemma ceilN x : ceil (- x) = - floor x. Proof. by rewrite /ceil opprK. Qed.
-
-Lemma floorN x : floor (- x) = - ceil x. Proof. by rewrite /ceil opprK. Qed.
+Proof. by []. Qed.
 
-Lemma abs_ceil_ge x : `|x| <= `|ceil x|.+1%:R.
-Proof.
-rewrite -natr1 natr_absz; have [x0|x0] := ltP 0%R x.
-  by rewrite !gtr0_norm ?ceil_gt0// (le_trans (ceil_ge _))// lerDl.
-by rewrite !ler0_norm ?ceil_le0// /ceil opprK; exact/ltW/lt_succ_floor.
-Qed.
+#[deprecated(since="mathcomp-analysis 1.3.0", note="use `Num.Theory.ceil_le` instead")]
+Lemma le_ceil : {homo @Num.ceil R : x y / x <= y}.
+Proof. exact: ceil_le. Qed.
 
 End CeilTheory.
 
diff --git a/theories/sequences.v b/theories/sequences.v
index cdd82622d..703fae4aa 100644
--- a/theories/sequences.v
+++ b/theories/sequences.v
@@ -1,7 +1,7 @@
 (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
 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 boolp classical_sets functions.
 From mathcomp Require Import set_interval.
 Require Import reals ereal signed topology normedtype landau.
 
@@ -92,6 +92,7 @@ Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 Import Order.TTheory GRing.Theory Num.Def Num.Theory.
 Import numFieldNormedType.Exports.
+From mathcomp Require Import mathcomp_extra.
 
 Local Open Scope classical_set_scope.
 Local Open Scope ring_scope.
@@ -1274,9 +1275,9 @@ Proof.
 rewrite /series; near \oo => N; have xN : x < N%:R; last first.
   rewrite -(@is_cvg_series_restrict N.+1).
   by apply: (nondecreasing_is_cvgn (incr_S1 N)); eexists; apply: S1_sup.
-near: N; exists (absz (reals.floor x)).+1 => // m; rewrite /mkset -(@ler_nat R).
-move/lt_le_trans => -> //; rewrite (lt_le_trans (reals.lt_succ_floor x)) // -addn1.
-by rewrite natrD lerD2r -(@gez0_abs (reals.floor x)) ?reals.floor_ge0// ltW.
+near: N; exists `|floor x|.+1 => // m; rewrite /mkset -(@ler_nat R).
+move/lt_le_trans => -> //; rewrite (lt_le_trans (lt_succ_floor x))//.
+by rewrite -intrD1 -natr1 lerD2r -(@gez0_abs (floor x)) ?floor_ge0// ltW.
 Unshelve. all: by end_near. Qed.
 
 End exponential_series_cvg.
diff --git a/theories/topology.v b/theories/topology.v
index 82834994d..a9230bead 100644
--- a/theories/topology.v
+++ b/theories/topology.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 archimedean.
 From mathcomp Require Import boolp classical_sets functions.
-From mathcomp Require Import cardinality mathcomp_extra fsbigop.
+From mathcomp Require Import cardinality fsbigop.
 Require Import reals signed.
 
 (**md**************************************************************************)
@@ -447,6 +447,7 @@ Unset Printing Implicit Defensive.
 Obligation Tactic := idtac.
 
 Import Order.TTheory GRing.Theory Num.Theory.
+From mathcomp Require Import mathcomp_extra.
 Local Open Scope classical_set_scope.
 Local Open Scope ring_scope.
 
@@ -2281,7 +2282,7 @@ Proof. by exists N. Qed.
 Lemma nbhs_infty_ger {R : realType} (r : R) :
   \forall n \near \oo, (r <= n%:R)%R.
 Proof.
-exists (`|ceil r|)%N => // n /=; rewrite -(ler_nat R); apply: le_trans.
+exists `|Num.ceil r|%N => // n /=; rewrite -(ler_nat R); apply: le_trans.
 by rewrite (le_trans (ceil_ge _))// natr_absz ler_int ler_norm.
 Qed.
 
@@ -4988,9 +4989,11 @@ apply/countable_uniformityP.
 exists (fun n => [set xy : T * T | ball xy.1 n.+1%:R^-1 xy.2]); last first.
   by move=> n; exact: (entourage_ball _ n.+1%:R^-1%:pos).
 move=> E; rewrite -entourage_ballE => -[e e0 subE].
-exists `|floor e^-1|%N; apply: subset_trans subE => xy; apply: le_ball.
+exists `|Num.floor e^-1|%N; apply: subset_trans subE => xy; apply: le_ball.
 rewrite /= -[leRHS]invrK lef_pV2 ?posrE ?invr_gt0// -natr1.
-by rewrite natr_absz ger0_norm ?floor_ge0 ?invr_ge0// 1?ltW// reals.lt_succ_floor.
+rewrite natr_absz ger0_norm; last first.
+  by rewrite -floor_ge_int ?invr_ge0// ltW.
+by rewrite intrD1 ltW// lt_succ_floor.
 Qed.
 
 (** Specific pseudoMetric spaces *)
@@ -4998,16 +5001,20 @@ Qed.
 (** matrices *)
 Section matrix_PseudoMetric.
 Variables (m n : nat) (R : numDomainType) (T : pseudoMetricType R).
-Implicit Types x y : 'M[T]_(m, n).
-Definition mx_ball x (e : R) y := forall i j, ball (x i j) e (y i j).
-Lemma mx_ball_center x (e : R) : 0 < e -> mx_ball x e x.
-Proof. by move=> ???; apply: ballxx. Qed.
-Lemma mx_ball_sym x y (e : R) : mx_ball x e y -> mx_ball y e x.
-Proof. by move=> xe_y ??; apply/ball_sym/xe_y. Qed.
-Lemma mx_ball_triangle x y z (e1 e2 : R) :
+Implicit Types (x y : 'M[T]_(m, n)) (e : R).
+
+Definition mx_ball x e y := forall i j, ball (x i j) e (y i j).
+
+Lemma mx_ball_center x e : 0 < e -> mx_ball x e x.
+Proof. by move=> ? ? ?; exact: ballxx. Qed.
+
+Lemma mx_ball_sym x y e : mx_ball x e y -> mx_ball y e x.
+Proof. by move=> xe_y ? ?; apply/ball_sym/xe_y. Qed.
+
+Lemma mx_ball_triangle x y z e1 e2 :
   mx_ball x e1 y -> mx_ball y e2 z -> mx_ball x (e1 + e2) z.
 Proof.
-by move=> xe1_y ye2_z ??; apply: ball_triangle; [apply: xe1_y| apply: ye2_z].
+by move=> xe1_y ye2_z ??; apply: ball_triangle; [exact: xe1_y|exact: ye2_z].
 Qed.
 
 Lemma mx_entourage : entourage = entourage_ mx_ball.
@@ -5016,14 +5023,14 @@ rewrite predeqE=> A; split; last first.
   move=> [_/posnumP[e] sbeA].
   by exists (fun _ _ => [set xy | ball xy.1 e%:num xy.2]).
 move=> [P]; rewrite -entourage_ballE => entP sPA.
-set diag := fun (e : {posnum R}) => [set xy : T * T | ball xy.1 e%:num xy.2].
+set diag := fun e : {posnum R} => [set xy : T * T | ball xy.1 e%:num xy.2].
 exists (\big[Num.min/1%:pos]_i \big[Num.min/1%:pos]_j xget 1%:pos
   (fun e : {posnum R} => diag e `<=` P i j))%:num => //=.
 move=> MN MN_min; apply: sPA => i j.
 have /(xgetPex 1%:pos): exists e : {posnum R}, diag e `<=` P i j.
   by have [_/posnumP[e]] := entP i j; exists e.
 apply; apply: le_ball (MN_min i j).
-apply: le_trans (@bigmin_le _ [the orderType _ of {posnum R}] _ _ i _) _.
+apply: le_trans (@bigmin_le _ {posnum R} _ _ i _) _.
 exact: bigmin_le.
 Qed.
 
@@ -5675,21 +5682,23 @@ Qed.
 Local Open Scope classical_set_scope.
 Local Open Scope ring_scope.
 
-Local Definition distN (e : R) : nat := `|floor e^-1|%N.
+Local Definition distN (e : R) : nat := `|Num.floor e^-1|%N.
 
 Local Lemma distN0 : distN 0 = 0%N.
-Proof. by rewrite /distN invr0 reals.floor0. Qed.
+Proof. by rewrite /distN invr0 floor0. Qed.
 
-Local Lemma distN_nat (n : nat): distN (n%:R^-1) = n.
+Local Lemma distN_nat (n : nat) : distN n%:R^-1 = n.
 Proof.
-by rewrite /distN invrK floor_natz -[RHS]distn0; congr absz; rewrite subr0 intz.
+rewrite /distN invrK.
+apply/eqP; rewrite -(@eqr_nat R) natr_absz ger0_norm ?floor_ge0//.
+by rewrite -intrEfloor intrEge0.
 Qed.
 
 Local Lemma distN_le e1 e2 : e1 > 0 -> e1 <= e2 -> (distN e2 <= distN e1)%N.
 Proof.
 move=> e1pos e1e2; rewrite /distN; apply: lez_abs2.
   by rewrite floor_ge0 ltW// invr_gt0 (lt_le_trans _ e1e2).
-by rewrite le_floor// lef_pV2 ?invrK ?invr_gt0//; exact: (lt_le_trans _ e1e2).
+by rewrite floor_le// lef_pV2 ?invrK ?invr_gt0//; exact: (lt_le_trans _ e1e2).
 Qed.
 
 Local Fixpoint n_step_ball n x e z :=
@@ -5819,7 +5828,7 @@ move: e1 e2 x z; elim: n.
       rewrite -[e2]addr0 -(subrr e1) addrA -lerBlDr opprK addrC.
       by rewrite [e2 + _]addrC -deE; exact: lerD.
     - by rewrite addn0.
-  move=> /negP; rewrite -real_ltNge ?num_real //.
+  move=> /negP; rewrite -ltNge//.
   move=> e1d1; exists y, z, 0%N, 0%N; split.
   - by apply: n_step_ball_le; last (exact: Oxy); exact: ltW.
   - rewrite -deE; apply: (@n_step_ball_le _ _ d2) => //.
@@ -5837,7 +5846,7 @@ case: (pselect (e2 <= d2)).
   - by rewrite addn0.
 have d1E' : d1 = e1 + (e2 - d2).
   by move: deE; rewrite addrA [e1 + _]addrC => <-; rewrite -addrA subrr addr0.
-move=> /negP; rewrite -?real_ltNge // ?num_real // => d2lee2.
+move=> /negP; rewrite -ltNge// => d2lee2.
   case: (IH e1 (e2 - d2) x y); rewrite ?subr_gt0 // -d1E' //.
   move=> t1 [t2] [c1] [c2] [] Oxy1 gt1t2 t2y <-.
   exists t1, t2, c1, c2.+1; split => //.
@@ -5896,7 +5905,7 @@ Lemma countable_uniform_bounded (x y : T) :
   in @ball _ U x 2 y.
 Proof.
 rewrite /ball; exists O%N; rewrite /n_step_ball; split; rewrite // /distN.
-suff -> : @floor R 2^-1 = 0 by rewrite absz0 /=.
+rewrite [X in `|X|%N](_ : _ = 0) ?absz0//.
 apply/eqP; rewrite -[_ == _]negbK; rewrite floor_neq0 negb_or -?ltNge -?leNgt.
 by apply/andP; split => //; rewrite invf_lt1 //= ltrDl.
 Qed.