Adapt to math-comp/math-comp#1469

Author: proux01

classical/mathcomp_extra.v

@@ -147,22 +147,22 @@ Context {R : archiDomainType}.
 Implicit Type x : R.
 
 Lemma ge_floor x : (Num.floor x)%:~R <= x.
-Proof. exact: Num.Theory.ge_floor. Qed.
+Proof. exact: Num.Theory.floor_le_tmp. Qed.
 
 #[deprecated(since="mathcomp 2.4.0", note="Use floor_ge_int_tmp instead.")]
 Lemma floor_ge_int x (z : int) : (z%:~R <= x) = (z <= Num.floor x).
-Proof. exact: Num.Theory.floor_ge_int. Qed.
+Proof. by rewrite floor_ge_int_tmp. Qed.
 
 Lemma lt_succ_floor x : x < (Num.floor x + 1)%:~R.
 Proof. exact: Num.Theory.lt_succ_floor. 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.
+Proof. exact: Num.Theory.ceil_ge. 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.
+Proof. by rewrite Num.Theory.ceil_le_int_tmp. Qed.
 
 Lemma ceilN x : Num.ceil (- x) = - Num.floor x.
 Proof. by rewrite ?ceilNfloor /Num.ceil opprK. Qed.
@@ -331,7 +331,7 @@ by move=> ?; rewrite [RHS]real_ltNge ?realz -?real_floor_ge_int_tmp -?ltNge.
 Qed.
 
 Lemma le_floor : {homo (@Num.floor R) : x y / x <= y}.
-Proof. exact: floor_le. Qed.
+Proof. exact: le_floor. Qed.
 
 Lemma real_floor_eq x n : x \is Num.real ->
   (Num.floor x == n) = (n%:~R <= x < (n + 1)%:~R).
@@ -392,7 +392,7 @@ by move=> xr; apply/eqP/idP => [<-|]; [exact: real_ceil_itv|exact: ceil_def].
 Qed.
 
 Lemma le_ceil_tmp : {homo (@Num.ceil R) : x y / x <= y}.
-Proof. exact: ceil_le. Qed.
+Proof. exact: le_ceil_tmp. Qed.
 
 Lemma real_ceil_ge0 x : x \is Num.real -> (0 <= Num.ceil x) = (-1 < x).
 Proof.

classical/unstable.v

@@ -363,7 +363,7 @@ Implicit Type x : R.
 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 !gtr0_norm ?ceil_gt0// (le_trans (Num.Theory.ceil_ge _))// lerDl.
 by rewrite !ler0_norm ?ceil_le0// ?ceilNfloor opprK intrD1 ltW// floorD1_gt.
 Qed.
 

reals/reals.v

@@ -507,7 +507,7 @@ Lemma Rfloor0 : Rfloor 0 = 0 :> R. Proof. by rewrite /Rfloor floor0. Qed.
 Lemma Rfloor1 : Rfloor 1 = 1 :> R. Proof. by rewrite /Rfloor floor1. Qed.
 
 Lemma le_Rfloor : {homo (@Rfloor R) : x y / x <= y}.
-Proof. by move=> x y /Num.Theory.floor_le; rewrite ler_int. Qed.
+Proof. by move=> x y /Num.Theory.le_floor; rewrite ler_int. Qed.
 
 Lemma Rfloor_ge_int x (n : int) : (n%:~R <= x)= (n%:~R <= Rfloor x).
 Proof. by rewrite ler_int floor_ge_int. Qed.
@@ -541,20 +541,20 @@ Lemma Rceil0 : Rceil 0 = 0 :> R.
 Proof. by rewrite /Rceil ceil0. Qed.
 
 Lemma Rceil_ge x : x <= Rceil x.
-Proof. by rewrite Num.Theory.le_ceil ?num_real. Qed.
+Proof. by rewrite Num.Theory.ceil_ge ?num_real. Qed.
 
 Lemma le_Rceil : {homo (@Rceil R) : x y / x <= y}.
-Proof. by move=> x y ?; rewrite /Rceil ler_int ceil_le. Qed.
+Proof. by move=> x y ?; rewrite /Rceil ler_int le_ceil_tmp. Qed.
 
 Lemma Rceil_ge0 x : 0 <= x -> 0 <= Rceil x.
-Proof. by move=> x0; rewrite /Rceil ler0z -(ceil0 R) ceil_le. Qed.
+Proof. by move=> x0; rewrite /Rceil ler0z -(ceil0 R) le_ceil_tmp. Qed.
 
 Lemma RceilE x : Rceil x = (ceil x)%:~R.
 Proof. by []. 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.
+Proof. exact: le_ceil_tmp. Qed.
 
 End CeilTheory.
 

theories/measurable_realfun.v

@@ -646,7 +646,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// ?le_ceil// ceil_gt0.
+by rewrite natr_absz gtr0_norm// ?ceil_ge// ceil_gt0.
 Qed.
 
 End erealwithrays.

theories/normedtype_theory/num_normedtype.v

@@ -499,7 +499,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 pmulrn ceil_le_int// [ceil _]intEsign.
+rewrite pmulrn -ceil_le_int_tmp [ceil _]intEsign.
 by rewrite le_gtF ?expr0 ?mul1r ?lez_nat ?ceil_ge0//; near: n; apply: Foo.
 Unshelve. all: by end_near. Qed.
 
@@ -591,7 +591,7 @@ move=> dF nyF; rewrite itvNy_bnd_bigcup_BLeft eqEsubset; split.
     move/cvgrNy_lt : nyF => /(_ (F a - n%:R))[z [zreal zFan]].
     exists `|ceil (a - z)|%N.
     rewrite zFan// ltrBlDr -ltrBlDl.
-    rewrite (le_lt_trans (Num.Theory.le_ceil _)) ?num_real//.
+    rewrite (le_lt_trans (Num.Theory.ceil_ge _)) ?num_real//.
     by rewrite (le_lt_trans (ler_norm _))// -natr1 -intr_norm ltrDl.
   by exists i => //=; rewrite in_itv/= yFa andbT (lt_le_trans _ Fany).
 - move=> z/= [n _ /=]; rewrite in_itv/= => /andP[Fanz zFa].