diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index c52d4873e7..d1109a9c83 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -24,6 +24,15 @@
   + lemmas `g_sigma_completed_algebra_genE`, `negligible_sub_caratheodory`,
     `completed_caratheodory_measurable`
 
+- in `reals.v`:
+  + lemma `mem_rg1_floor`
+
+- in `mathcomp_extra.v`:
+  + lemma `ge_floor`
+
+- in `mathcomp_extra.v`:
+  + lemmas `intr1`, `int1r`, `natr_def`
+
 ### Changed
 
 - in `topology.v`:
@@ -31,6 +40,17 @@
     `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_le0`, `floor_lt0`, `floor_natz`,
+    `floor_ge_int`, `floor_neq0`, `floor_lt_int`, `ceil_ge`, `ceil_ge0`, `ceil_gt0`,
+    `ceil_le0`, `ceil_ge_int`, `ceil_lt_int`, `ceilN`, `abs_ceil_ge`
+
 ### Renamed
 
 - in `constructive_ereal.v`:
@@ -56,8 +76,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 0e82043f43..8952390cd1 100644
--- a/classical/mathcomp_extra.v
+++ b/classical/mathcomp_extra.v
@@ -374,3 +374,83 @@ by elim: p => //= p <-;
 Qed.
 
 End positive.
+
+Lemma intr1 {R : ringType} (i : int) : i%:~R + 1 = (i + 1)%:~R :> R.
+Proof. by rewrite intrD. Qed.
+
+Lemma int1r {R : ringType} (i : int) : 1 + i%:~R = (1 + i)%:~R :> R.
+Proof. by rewrite intrD. Qed.
+
+From mathcomp Require Import archimedean.
+
+Lemma natr_def (n : int) : (n \is a Num.nat) = (0 <= n)%R.
+Proof. by []. Qed.
+
+Section floor_ceil.
+Context {R : archiDomainType}.
+Implicit Type x : R.
+
+Lemma ge_floor x : (Num.floor x)%:~R <= x.
+Proof. by rewrite Num.Theory.ge_floor. Qed.
+
+Lemma floor_ge0 x : (0 <= Num.floor x) = (0 <= x).
+Proof. by rewrite -Num.Theory.floor_ge_int. Qed.
+
+Lemma floor_le0 x : x <= 0 -> Num.floor x <= 0.
+Proof. by move/Num.Theory.floor_le; rewrite Num.Theory.floor0. Qed.
+
+Lemma floor_lt0 x : x < 0 -> Num.floor x < 0.
+Proof. by move=> x0; rewrite -(@ltrz0 R) (le_lt_trans (ge_floor _)). Qed.
+
+Lemma lt_succ_floor x : x < (Num.floor x + 1)%:~R.
+Proof. by rewrite Num.Theory.lt_succ_floor. Qed.
+
+Lemma floor_natz n : Num.floor (n%:R : R) = n%:~R :> int.
+Proof.
+by rewrite (@Num.Theory.floor_def _ _ n%:~R)// intr1 !mulrz_nat lexx/= ltr_nat addn1.
+Qed.
+
+Lemma floor_ge_int x (z : int) : (z%:~R <= x) = (z <= Num.floor x).
+Proof. by rewrite Num.Theory.floor_ge_int. Qed.
+
+Lemma floor_neq0 x : (Num.floor x != 0) = (x < 0) || (x >= 1).
+Proof.
+apply/idP/orP => [|[x0|/Num.Theory.floor_le r1]]; first rewrite neq_lt => /orP[x0|x0].
+- by left; apply: contra_lt x0; rewrite -floor_ge_int.
+- by right; rewrite (le_trans _ (ge_floor _))// ler1z -gtz0_ge1.
+- by rewrite lt_eqF//; apply: contra_lt x0; rewrite -floor_ge_int.
+- by rewrite gt_eqF// (lt_le_trans _ r1)// Num.Theory.floor1.
+Qed.
+
+Lemma floor_lt_int x (z : int) : (x < z%:~R) = (Num.floor x < z).
+Proof. by rewrite ltNge Num.Theory.floor_ge_int// -ltNge. Qed.
+
+Lemma ceil_ge x : x <= (Num.ceil x)%:~R.
+Proof. by rewrite Num.Theory.le_ceil. Qed.
+
+Lemma ceil_ge0 x : 0 <= x -> 0 <= Num.ceil x.
+Proof. by move/(ge_trans (ceil_ge x)); rewrite -(ler_int R). Qed.
+
+Lemma ceil_gt0 x : 0 < x -> 0 < Num.ceil x.
+Proof. by move=> ?; rewrite oppr_gt0 floor_lt0 // ltrNl oppr0. Qed.
+
+Lemma ceil_le0 x : x <= 0 -> Num.ceil x <= 0.
+Proof. by move=> x0; rewrite -lerNl oppr0 floor_ge0 -lerNr oppr0. Qed.
+
+Lemma ceil_ge_int x (z : int) : (x <= z%:~R) = (Num.ceil x <= z).
+Proof. by rewrite Num.Theory.ceil_le_int. Qed.
+
+Lemma ceil_lt_int x (z : int) : (z%:~R < x) = (z < Num.ceil x).
+Proof. by rewrite ltNge ceil_ge_int -ltNge. Qed.
+
+Lemma ceilN x : Num.ceil (- x) = - Num.floor x.
+Proof. by rewrite /Num.ceil opprK. Qed.
+
+Lemma abs_ceil_ge x : `|x| <= `|Num.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// opprK intr1 ltW// lt_succ_floor.
+Qed.
+
+End floor_ceil.
diff --git a/theories/altreals/realsum.v b/theories/altreals/realsum.v
index c5eac8ae63..886773498e 100644
--- a/theories/altreals/realsum.v
+++ b/theories/altreals/realsum.v
@@ -2,9 +2,8 @@
 (* 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.
@@ -142,16 +141,16 @@ 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.
+  pose j := `|Num.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.
+  rewrite gez0_abs ?floor_ge0 ?invr_ge0 ?normr_ge0//.
+  by rewrite intr1 mathcomp_extra.lt_succ_floor.
 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/finiteNP; pose j := `|Num.floor (M / i.+1%:R)|.+1.
+pose K := (`|Num.floor M|.+1 * i.+1)%N; move/(_ K)/asboolP/exists_asboolP.
 move=> 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.
@@ -160,9 +159,10 @@ apply/(@lt_le_trans _ _ (\sum_(x : J) 1 / i.+1%:~R)); last first.
   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.
+have /andP[_] := mem_rg1_floor M; rewrite -addn1.
+by rewrite natrD /= mulr1n pmulrn -{1}[Num.floor _]gez0_abs // floor_ge0.
 Qed.
+
 End SummableCountable.
 
 (* -------------------------------------------------------------------- *)
@@ -1201,9 +1201,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 4d2fcce6fa..3408745267 100644
--- a/theories/ereal.v
+++ b/theories/ereal.v
@@ -1266,7 +1266,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 +1276,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 +1402,24 @@ 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.
-      by rewrite Znat_def floor_ge0 le_max lexx orbC.
+    have /natrP[N Nfloor] : Num.floor (Num.max d 0%R) \is a Num.nat.
+      by rewrite natr_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.
-    by rewrite Znat_def floor_ge0 le_max lexx orbC.
+    apply; rewrite (lt_le_trans (mathcomp_extra.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 natr_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.
-  by rewrite Znat_def floor_ge0.
+  apply; rewrite (lt_le_trans (mathcomp_extra.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 natr_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.
+rewrite (lt_le_trans (mathcomp_extra.lt_succ_floor _))// Nfloor.
+by rewrite !natr1 mulrz_nat ler_nat.
 Qed.
diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v
index 16910f7264..9ca1e3de0b 100644
--- a/theories/lebesgue_integral.v
+++ b/theories/lebesgue_integral.v
@@ -1287,22 +1287,22 @@ 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 -bigcup_seq /=; exists `|floor (r * 2 ^+ n.+1)|%N.
     rewrite /= mem_index_iota; apply/andP; split.
-      rewrite -ltez_nat gez0_abs ?reals.floor_ge0; last first.
+      rewrite -ltez_nat gez0_abs ?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.
+      apply: (@le_trans _ _ (floor (n * 2 ^ n.+1)%:R)); last first.
+        by apply: floor_le; rewrite natrM natrX ler_pM2r.
+      by rewrite -floor_ge_int.
     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 _))//.
+    rewrite -(@ltr_int R) (le_lt_trans (ge_floor _)) ?num_real//.
     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.
+    rewrite ler_pdivrMr// (le_trans _ (ge_floor _)) ?num_real//.
+    by rewrite -(@gez0_abs (floor _))// floor_ge0 mulr_ge0// (le_trans _ nr).
+  rewrite ltr_pdivlMr// (lt_le_trans (mathcomp_extra.lt_succ_floor _))//.
+  rewrite -[in leRHS]natr1 -intr1 lerD2r// -(@gez0_abs (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.
@@ -1430,18 +1430,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 _)) ?num_real// 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 _)) ?num_real//.
+    by rewrite -(@gez0_abs (floor _))// floor_ge0 mulr_ge0// ltW.
+  rewrite ltr_pdivlMr// (lt_le_trans (mathcomp_extra.lt_succ_floor _))//.
+  rewrite -[in leRHS]natr1 -intr1 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 +1539,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 intr1 mathcomp_extra.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 +1579,21 @@ 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.
+  by rewrite -(@gez0_abs (ceil _)) // ceil_ge0.
 - move/cvgrPdist_lt => /(_ _ ltr01) -[n _].
-  move=> /(_ (`|reals.floor l|.+1 + n)%N) /= /(_ (leq_addl _ _)).
+  move=> /(_ (`|floor 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// 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 (@le_trans _ _ (- floor l)%:~R) //.
+    by rewrite mulrNz lerNl opprK ge_floor.
+  by rewrite -(@lez0_abs (floor _))// floor_le0 // ltW.
 Qed.
 
 Lemma ecvg_approx (f0 : forall x, D x -> (0 <= f x)%E) x :
@@ -2346,7 +2347,7 @@ 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 lt0_mulye//; apply/cvgeNyPleNy; near=> M;
@@ -2355,7 +2356,7 @@ transitivity (\int[mu]_(x in D) limn (g^~ x)).
       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.
@@ -2377,7 +2378,7 @@ 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//.
 by rewrite mulr_ge0// ?invr_ge0//; exact/fine_ge0/integral_ge0.
@@ -2608,7 +2609,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 +2618,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,7 +3439,7 @@ 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 _ _)).
@@ -3686,7 +3687,7 @@ 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.
@@ -6456,7 +6457,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 +6659,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 3a85507b30..e5fb6d24f7 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.
@@ -1155,12 +1155,12 @@ rewrite [X in measurable X](_ : _ =
                           exact: emeasurable_fun_infty_c].
 rewrite predeqE => t; split => [/= [Dt ft]|].
   have [ft0|ft0] := leP 0%R (fine (f t)).
-    exists `|ceil (fine (f t))|%N => //=; split => //; split.
+    exists `|(ceil (fine (f t)))%real|%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.
-  exists `|floor (fine (f t))|%N => //=; split => //; split.
+  exists `|(floor (fine (f t)))%real|%N => //=; split => //; split.
     rewrite natr_absz ltr0_norm ?floor_lt0// EFinN.
-    by rewrite -{2}(fineK ft) lee_fin mulrNz opprK floor_le.
+    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.
@@ -1403,18 +1403,18 @@ Lemma eset1Ny :
 Proof.
 rewrite eqEsubset; split=> [_ -> i _ |]; first by rewrite /= in_itv /= ltNyr.
 move=> [r|/(_ O Logic.I)|]//.
-move=> /(_ `|floor r|%N Logic.I); rewrite /= in_itv/= ltNge.
+move=> /(_ `|(floor r)%real|%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 mulrNz lerNl opprK ge_floor.
 Qed.
 
 Lemma eset1y : [set +oo] = \bigcap_k `]k%:R%:E, +oo[%classic :> set (\bar R).
 Proof.
 rewrite eqEsubset; split=> [_ -> i _/=|]; first by rewrite in_itv /= ltry.
-move=> [r| |/(_ O Logic.I)] // /(_ `|ceil r|%N Logic.I); rewrite /= in_itv /=.
+move=> [r| |/(_ O Logic.I)] // /(_ `|(ceil r)%real|%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.
@@ -2400,7 +2400,7 @@ have {}EBr2 : \esum_(i in E) mu (closure (B i)) <=
   by apply: bigcup_measurable => *; exact: measurable_closure.
 have finite_set_F i : finite_set (F i).
   apply: contrapT.
-  pose M := `|ceil ((r%:num + 2) *+ 2 / (1 / (2 ^ i.+1)%:R))|.+1.
+  pose M := `|(ceil ((r%:num + 2) *+ 2 / (1 / (2 ^ i.+1)%:R)))%real|.+1.
   move/(infinite_set_fset M) => [/= C] CsubFi McardC.
   have MC : (M%:R * (1 / (2 ^ i.+1)%:R))%:E <=
             mu (\bigcup_(j in [set` C]) closure (B j)).
diff --git a/theories/lebesgue_stieltjes_measure.v b/theories/lebesgue_stieltjes_measure.v
index f4c6d42170..f6647899a3 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|%R)%real + 1)%R|%N; rewrite //= in_itv/=.
+  rewrite !natr_absz intr_norm intrD.
+  suff: `|x| < `|(floor `|x|)%real%:~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 intr1 (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 59f84235dc..e8fad5b494 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.
@@ -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 6b5b67271f..64ed061c78 100644
--- a/theories/normedtype.v
+++ b/theories/normedtype.v
@@ -252,10 +252,10 @@ 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 => //.
+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.
@@ -596,7 +596,7 @@ 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.
+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.
 
@@ -4919,7 +4919,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 +5763,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 +5779,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// mathcomp_extra.ge_floor.
 Qed.
 
 Lemma cover_vitali_collection_partition :
diff --git a/theories/real_interval.v b/theories/real_interval.v
index cc90e5e51f..ce860e82a5 100644
--- a/theories/real_interval.v
+++ b/theories/real_interval.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 fingroup perm rat archimedean finmap.
 From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
 From mathcomp Require Export set_interval.
 From HB Require Import structures.
@@ -176,7 +176,8 @@ 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.
+rewrite -natr1 natr_absz ger0_norm ?floor_ge0 1?ltW//.
+by rewrite intr1 mathcomp_extra.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 intr1 ltW// mathcomp_extra.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 intr1 mathcomp_extra.lt_succ_floor.
 Qed.
 
 Lemma itv_bnd_open_bigcup (R : realType) b (r s : R) :
@@ -375,7 +377,7 @@ 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.
@@ -424,7 +426,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 ?intr1 ?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 1507cc6eb2..2e78a8ded5 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,7 +184,7 @@ 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.
 move=> /cvgrPdist_lt/(_ e%:num (ltac:(by [])))[] n _ /(_ _ (leqnn _)).
@@ -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 cf231eb6e7..92d228f78d 100644
--- a/theories/reals.v
+++ b/theories/reals.v
@@ -32,10 +32,8 @@
 (*     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)                                              *)
 (* ```                                                                        *)
 (*                                                                            *)
 (******************************************************************************)
@@ -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,26 @@ 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_Rfloor x : (range1 (Rfloor x)) x.
+Lemma mem_rg1_floor x : (range1 (floor x)%:~R) 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.
+rewrite /range1 /mkset intr1 mathcomp_extra.lt_succ_floor andbT.
+by rewrite mathcomp_extra.ge_floor.
 Qed.
 
+Lemma mem_rg1_Rfloor x : (range1 (Rfloor x)) x.
+Proof. by rewrite /Rfloor; 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 mathcomp_extra.ge_floor. Qed.
 
 Lemma lt_succ_Rfloor x : x < Rfloor x + 1.
 Proof. by case/andP: (mem_rg1_Rfloor x). Qed.
@@ -518,11 +506,9 @@ 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.
@@ -546,44 +532,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. by move=> a b ab; rewrite 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 +542,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 -mathcomp_extra.floor_ge_int// invr_ge0 subr_ge0 ltW.
+by rewrite intr1 mathcomp_extra.lt_succ_floor.
 Qed.
 
 End FloorTheory.
@@ -603,54 +554,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 cdd82622d6..da6077f95a 100644
--- a/theories/sequences.v
+++ b/theories/sequences.v
@@ -1274,9 +1274,10 @@ 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 (absz (floor x)).+1 => // m; rewrite /mkset -(@ler_nat R).
+move/lt_le_trans => -> //.
+rewrite (lt_le_trans (mathcomp_extra.lt_succ_floor x))//.
+by rewrite -intr1 -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 82834994df..59039eebc7 100644
--- a/theories/topology.v
+++ b/theories/topology.v
@@ -2281,7 +2281,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 +4988,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 -mathcomp_extra.floor_ge_int ?invr_ge0// ltW.
+by rewrite intr1 ltW// mathcomp_extra.lt_succ_floor.
 Qed.
 
 (** Specific pseudoMetric spaces *)
@@ -4999,11 +5001,15 @@ Qed.
 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) :
   mx_ball x e1 y -> mx_ball y e2 z -> mx_ball x (e1 + e2) z.
 Proof.
@@ -5675,21 +5681,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 +5827,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 +5845,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 +5904,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.