diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index d1109a9c83..a963ab4225 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -31,7 +31,7 @@
   + lemma `ge_floor`
 
 - in `mathcomp_extra.v`:
-  + lemmas `intr1`, `int1r`, `natr_def`
+  + lemmas `intr1`, `int1r`
 
 ### Changed
 
diff --git a/classical/mathcomp_extra.v b/classical/mathcomp_extra.v
index 8952390cd1..c0fc66e958 100644
--- a/classical/mathcomp_extra.v
+++ b/classical/mathcomp_extra.v
@@ -383,9 +383,6 @@ 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.
diff --git a/theories/Rstruct.v b/theories/Rstruct.v
index 4144f27165..903d00db69 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.
diff --git a/theories/ereal.v b/theories/ereal.v
index 3408745267..5c537d399d 100644
--- a/theories/ereal.v
+++ b/theories/ereal.v
@@ -5,7 +5,7 @@
 (* Copyright (c) - 2016--2018 - Polytechnique                           *)
 (* -------------------------------------------------------------------- *)
 From HB Require Import structures.
-From mathcomp Require Import all_ssreflect all_algebra finmap archimedean.
+From mathcomp Require Import all_ssreflect all_algebra archimedean finmap.
 From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
 From mathcomp Require Import fsbigop cardinality set_interval.
 Require Import reals signed topology.
@@ -1403,19 +1403,19 @@ Proof.
 move=> P; rewrite /ereal_loc_seq.
 case: x => /= [x [_/posnumP[d] dP] |[d [dreal dP]] |[d [dreal dP]]]; last 2 first.
     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.
+      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.
     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.
+    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.
   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.
+  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.