rm natr_def

math-comp · Jul 11, 2024 · 8bd8a06 · 8bd8a06
1 parent ea497da
commit 8bd8a06
Show file tree

Hide file tree

Showing 4 changed files with 7 additions and 9 deletions.
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
@@ -34,7 +34,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
@@ -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
@@ -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
@@ -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.