diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 4fb22e3961..432a61c508 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -6,16 +6,16 @@
 
 - in `reals.v`:
   + lemma `mem_rg1_floor`
+  + lemma `ge_floor`
 
 - in `mathcomp_extra.v`:
-  + lemmas `intr1`, `int1r`
+  + lemmas `intr1`, `int1r`, `natr_def`
 
 ### Changed
 
 - in `reals.v`:
-  + definition `floor` now a notation (in `real_scope`)
-  + definition `ceil` now a notation (in `real_scope`)
   + definitions `Rceil`, `Rfloor`
+  + `lt_succ_floor`: conclusion changed to match `lt_succ_floor` in MathComp
 
 ### Renamed
 
@@ -29,8 +29,8 @@
 ### Removed
 
 - in `reals.v`:
-  + `lt_succ_floor` renamed to `__deprecated__lt_succ_floor`
-    (use `lt_succ_floor` from MathComp instead)
+  + definition `floor` (use `Num.floor` instead)
+  + definition `ceil` (use `Num.ceil` instead)
 
 ### Infrastructure
 
diff --git a/classical/mathcomp_extra.v b/classical/mathcomp_extra.v
index 32e15d43e5..81c0235446 100644
--- a/classical/mathcomp_extra.v
+++ b/classical/mathcomp_extra.v
@@ -380,3 +380,8 @@ 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.
diff --git a/theories/altreals/realsum.v b/theories/altreals/realsum.v
index 5c35bc01d7..7f8f5e86a6 100644
--- a/theories/altreals/realsum.v
+++ b/theories/altreals/realsum.v
@@ -142,16 +142,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|))%real|%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 intr1 lt_succ_floor// num_real.
+  by rewrite intr1 reals.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))%real|.+1.
-pose K := (`|(floor M)%real|.+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.
@@ -161,7 +161,7 @@ apply/(@lt_le_trans _ _ (\sum_(x : J) 1 / i.+1%:~R)); last first.
 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_floor M; rewrite -addn1.
-by rewrite natrD /= mulr1n pmulrn -{1}[(floor _)%real]gez0_abs // floor_ge0.
+by rewrite natrD /= mulr1n pmulrn -{1}[Num.floor _]gez0_abs // floor_ge0.
 Qed.
 
 End SummableCountable.
diff --git a/theories/ereal.v b/theories/ereal.v
index d3d5b59c18..cde34729e5 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,24 +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))%real \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.
-    apply; rewrite (lt_le_trans (lt_succ_floor _)) ?num_real//.
-    by rewrite Nfloor ler_nat addn1.
-  have /ZnatP [N Nfloor] : (floor (Num.max (- d)%R 0%R))%real \is a Znat.
-    by rewrite Znat_def floor_ge0 le_max lexx orbC.
+    apply; rewrite (lt_le_trans (reals.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.
-  apply; rewrite (lt_le_trans (lt_succ_floor _)) ?num_real//.
-  by rewrite Nfloor ler_nat addn1.
-have /ZnatP[N Nfloor] : (floor d%:num^-1)%real \is a Num.nat.
-  by rewrite Znat_def floor_ge0.
+  apply; rewrite (lt_le_trans (reals.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.
-rewrite (lt_le_trans (lt_succ_floor _)) ?num_real// Nfloor.
-by rewrite -intr1 lerD// ler_nat.
+rewrite (lt_le_trans (reals.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 82643e2b43..e1a6c3c562 100644
--- a/theories/lebesgue_integral.v
+++ b/theories/lebesgue_integral.v
@@ -1302,7 +1302,7 @@ rewrite predeqE => r; split => [/= /[!in_itv]/= /andP[nr rn1]|].
     rewrite ler_pdivrMr// (le_trans _ (ge_floor _)) ?num_real//.
     by rewrite -(@gez0_abs (floor _)%real)// floor_ge0 mulr_ge0// (le_trans _ nr).
   rewrite ltr_pdivlMr// (lt_le_trans (lt_succ_floor _)) ?num_real//.
-  rewrite -[in leRHS]natr1 -intr1 lerD2r// -(@gez0_abs (floor _)%real) ?num_real// floor_ge0.
+  rewrite -[in leRHS]natr1 -intr1 lerD2r// -(@gez0_abs (floor _)%real)// 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.
@@ -1543,7 +1543,7 @@ have : fine (f x) < n%:R.
   rewrite -(@ler_nat R); apply: lt_le_trans.
   rewrite -natr1 (_ : `| _ |%:R  = (floor (fine (f x)))%real%:~R); last first.
     by rewrite -[in RHS](@gez0_abs (floor _)%real)// floor_ge0//; exact/fine_ge0/f0.
-  by rewrite intr1 lt_succ_floor ?num_real.
+  by rewrite intr1 reals.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.
diff --git a/theories/measure.v b/theories/measure.v
index 11b3277292..0aac5f29c9 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.
@@ -2198,8 +2198,8 @@ Lemma infinite_card_dirac (A : set T) : infinite_set A ->
   \esum_(i in A) \d_ i A = +oo :> \bar R.
 Proof.
 move=> infA; apply/eqyP => r r0.
-have [B BA Br] := infinite_set_fset `|(ceil r)%real| infA.
-apply: esum_ge; exists [set` B] => //; apply: (@le_trans _ _ `|(ceil r)%real|%:R%:E).
+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.
 move: Br; rewrite -(@ler_nat R) -lee_fin => /le_trans; apply.
 rewrite (eq_fsbigr (cst 1))/=; last first.
@@ -2292,7 +2292,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 b8c49d1ee4..514f98887f 100644
--- a/theories/normedtype.v
+++ b/theories/normedtype.v
@@ -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// ge_floor// num_real.
+by rewrite natr_absz// ger0_norm// reals.ge_floor.
 Qed.
 
 Lemma cover_vitali_collection_partition :
diff --git a/theories/realfun.v b/theories/realfun.v
index d22962658d..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)|%real%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 _)).
@@ -233,8 +234,8 @@ have y_p : y_ n @[n --> \oo] --> p.
   rewrite ltrBlDr => /lt_le_trans; apply.
   rewrite addrC lerD2r -(invrK e) lef_pV2// ?posrE ?invr_gt0//.
   near: t.
-  exists `|ceil e^-1|%real%N => // k /= ek.
-  rewrite (le_trans (ceil_ge _))// (@le_trans _ _ `|ceil e^-1|%real%:~R)//.
+  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 move: ek;rewrite -(leq_add2r 1) !addn1 -(ltr_nat R) => /ltW.
 have /fine_cvgP[[m _ mfy_] /= _] := h _ (conj py_ y_p).
@@ -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 0bd6ff6f78..c346fcab10 100644
--- a/theories/reals.v
+++ b/theories/reals.v
@@ -97,9 +97,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.
@@ -238,13 +236,6 @@ Qed.
 End ToInt.
 
 (* -------------------------------------------------------------------- *)
-Reserved Notation "'floor' r" (at level 10).
-Notation "'floor' x" := (Num.floor x) : real_scope.
-
-Reserved Notation "'ceil' r" (at level 10).
-Notation "'ceil' x" := (Num.ceil x) : real_scope.
-
-Local Open Scope real_scope.
 
 Section RealDerivedOps.
 Variable R : realType.
@@ -344,14 +335,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.
 
@@ -479,11 +470,14 @@ Proof. by rewrite inE; exists (floor x). Qed.
 Lemma RfloorE x : Rfloor x = (floor x)%:~R.
 Proof. by []. Qed.
 
+Lemma lt_succ_floor x : x < (floor x + 1)%:~R.
+Proof. by rewrite lt_succ_floor// num_real. Qed.
+
+Lemma ge_floor x : (floor x)%:~R <= x.
+Proof. by rewrite ge_floor// num_real. Qed.
+
 Lemma mem_rg1_floor x : (range1 (floor x)%:~R) x.
-Proof.
-rewrite /range1 /mkset intr1 lt_succ_floor ?num_real// andbT.
-by rewrite ge_floor// num_real.
-Qed.
+Proof. by rewrite /range1 /mkset intr1 lt_succ_floor andbT ge_floor. Qed.
 
 Lemma mem_rg1_Rfloor x : (range1 (Rfloor x)) x.
 Proof. by rewrite /Rfloor; exact: mem_rg1_floor. Qed.
@@ -492,7 +486,7 @@ Lemma Rfloor_le x : Rfloor x <= x.
 Proof. by case/andP: (mem_rg1_Rfloor x). Qed.
 
 Lemma __deprecated__floor_le x : (floor x)%:~R <= x.
-Proof. by rewrite ge_floor ?num_real. 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.
@@ -557,16 +551,17 @@ Proof. by rewrite floor0. Qed.
 Lemma floor1 : floor (1 : R) = 1.
 Proof. by rewrite floor1. Qed.
 
-Lemma __deprecated__floor_ge0 x : (0 <= floor x) = (0 <= x).
-Proof. by rewrite -floor_ge_int// num_real. Qed.
+Lemma floor_ge_int x (z : int) : (z%:~R <= x) = (z <= floor x).
+Proof. by rewrite Rfloor_ge_int RfloorE ler_int. Qed.
+
+Lemma floor_ge0 x : (0 <= floor x) = (0 <= x).
+Proof. by rewrite -floor_ge_int. Qed.
 
 Lemma floor_le0 x : x <= 0 -> floor x <= 0.
 Proof. by move=> x0; rewrite -floor0 Num.Theory.floor_le. Qed.
 
 Lemma floor_lt0 x : x < 0 -> floor x < 0.
-Proof.
-by move=> x0; rewrite -(@ltrz0 R) (le_lt_trans (ge_floor _))// num_real.
-Qed.
+Proof. by move=> x0; rewrite -(@ltrz0 R) (le_lt_trans (ge_floor _)). Qed.
 
 Lemma le_floor : {homo @Num.floor R : x y / x <= y}.
 Proof. by move=> a b ab; rewrite Num.Theory.floor_le. Qed.
@@ -574,34 +569,26 @@ Proof. by move=> a b ab; rewrite Num.Theory.floor_le. 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_ge_int ?num_real.
-- by right; rewrite (le_trans _ (ge_floor _)) ?num_real// ler1z -gtz0_ge1.
-- by rewrite lt_eqF//; apply: contra_lt x0; rewrite -floor_ge_int ?num_real.
+- 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)// floor1.
 Qed.
 
-Lemma __deprecated__lt_succ_floor x : x < (floor x)%:~R + 1.
-Proof. by rewrite intr1 lt_succ_floor// num_real. 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.
-
 Lemma ltr_add_invr (y x : R) : y < x -> exists k, y + k.+1%:R^-1 < x.
 Proof.
 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_ge_int ?num_real// invr_ge0 subr_ge0 ltW.
-by rewrite intr1 lt_succ_floor ?num_real.
+  by rewrite -floor_ge_int// invr_ge0 subr_ge0 ltW.
+by rewrite intr1 lt_succ_floor.
 Qed.
 
 End FloorTheory.
-#[deprecated(since="mathcomp-analysis 1.3.0", note="use `floor_ge_int` instead")]
-Notation floor_ge0 := __deprecated__floor_ge0 (only parsing).
 
 Section CeilTheory.
 Variable R : realType.
@@ -638,6 +625,8 @@ Proof. by move=> ?; rewrite 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.
 
+(* TODO: rename because le_ceil means something else in archimedean,
+and any should be renamed real_le_ceil *)
 Lemma le_ceil : {homo @Num.ceil R : x y / x <= y}.
 Proof. by move=> x y xy; rewrite lerNl opprK le_floor // lerNl opprK. Qed.
 
@@ -656,8 +645,7 @@ 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.
-rewrite !ler0_norm ?ceil_le0// opprK.
-by rewrite intr1; apply/ltW/lt_succ_floor; rewrite num_real.
+by rewrite !ler0_norm ?ceil_le0// opprK intr1 ltW// lt_succ_floor.
 Qed.
 
 End CeilTheory.
diff --git a/theories/sequences.v b/theories/sequences.v
index cd4885366a..c033a8efcb 100644
--- a/theories/sequences.v
+++ b/theories/sequences.v
@@ -1276,7 +1276,7 @@ rewrite /series; near \oo => N; have xN : x < N%:R; last first.
   by apply: (nondecreasing_is_cvgn (incr_S1 N)); eexists; apply: S1_sup.
 near: N; exists (absz (floor x)%real).+1 => // m; rewrite /mkset -(@ler_nat R).
 move/lt_le_trans => -> //.
-rewrite (lt_le_trans (@lt_succ_floor _ x _)) ?num_real//.
+rewrite (lt_le_trans (@reals.lt_succ_floor _ x))//.
 by rewrite -intr1 -natr1 lerD2r -(@gez0_abs (floor x)%real) ?floor_ge0// ltW.
 Unshelve. all: by end_near. Qed.
 
diff --git a/theories/topology.v b/theories/topology.v
index 38261dfeca..138aa4b68f 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)%real|)%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,10 +4988,10 @@ 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)%real|%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.
-rewrite natr_absz ger0_norm ?floor_ge0 ?invr_ge0 1?ltW//.
-by rewrite intr1 lt_succ_floor// num_real.
+rewrite natr_absz ger0_norm; last by rewrite -reals.floor_ge_int ?invr_ge0// ltW.
+by rewrite intr1 ltW// reals.lt_succ_floor.
 Qed.
 
 (** Specific pseudoMetric spaces *)
@@ -5000,11 +5000,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.
@@ -5676,10 +5680,10 @@ Qed.
 Local Open Scope classical_set_scope.
 Local Open Scope ring_scope.
 
-Local Definition distN (e : R) : nat := `|(floor e^-1)%real|%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.
 Proof.
@@ -5822,7 +5826,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) => //.
@@ -5840,7 +5844,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 => //.