adressing comments (wip?)

CHANGELOG_UNRELEASED.md

@@ -34,7 +34,7 @@
   + lemma `ge_floor`
 
 - in `mathcomp_extra.v`:
-  + lemmas `intr1`, `int1r`
+  + lemmas `intr1D`, `intrD1`, `floor_eq`, `floorN`
 
 ### Changed
 
@@ -52,9 +52,11 @@
   + generalized to `archiDomainType`:
     lemmas `floor_ge0`, `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`
+    `ceil_le0`, `ceil_ge_int`, `ceilN`, `abs_ceil_ge`
   + generalized to `archiDomainType` and precondition generalized:
-    + `floor_le0`
+    * `floor_le0`
+  + generalized to `archiDomainType` and renamed:
+    * `ceil_lt_int` -> `ceil_gt_int`
 
 ### Renamed
 

classical/mathcomp_extra.v

@@ -375,10 +375,10 @@ Qed.
 
 End positive.
 
-Lemma intr1 {R : ringType} (i : int) : i%:~R + 1 = (i + 1)%:~R :> R.
+Lemma intrD1 {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.
+Lemma intr1D {R : ringType} (i : int) : 1 + i%:~R = (1 + i)%:~R :> R.
 Proof. by rewrite intrD. Qed.
 
 From mathcomp Require Import archimedean.
@@ -408,35 +408,49 @@ Proof. by rewrite -floor_lt_int. Qed.
 Lemma lt_succ_floor x : x < (Num.floor x + 1)%:~R.
 Proof. exact: Num.Theory.lt_succ_floor. Qed.
 
+Lemma floor_eq x m : (Num.floor x == m) = (m%:~R <= x < (m + 1)%:~R).
+Proof.
+apply/eqP/idP; [move=> <-|by move=> /Num.Theory.floor_def ->].
+by rewrite Num.Theory.ge_floor//= Num.Theory.lt_succ_floor.
+Qed.
+
 Lemma floor_neq0 x : (Num.floor x != 0) = (x < 0) || (x >= 1).
 Proof. by rewrite neq_lt -floor_lt_int gtz0_ge1 -floor_ge_int. 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.
 
+#[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.
 
-Lemma ceil_lt_int x (z : int) : (z%:~R < x) = (z < Num.ceil x).
-Proof. by rewrite ltNge ceil_ge_int -ltNge. Qed.
+Lemma ceil_gt_int x (z : int) : (z%:~R < x) = (z < Num.ceil x).
+Proof. by rewrite ltNge Num.Theory.ceil_le_int// -ltNge. Qed.
+
+Lemma ceilN x : Num.ceil (- x) = - Num.floor x.
+Proof. by rewrite /Num.ceil opprK. 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 floorN x : Num.floor (- x) = - Num.ceil x.
+Proof. by rewrite /Num.ceil opprK. Qed.
 
-Lemma ceil_gt0 x : 0 < x -> 0 < Num.ceil x.
-Proof. by rewrite -ceil_lt_int. Qed.
+Lemma ceil_ge0 x : (- 1 < x) = (0 <= Num.ceil x).
+Proof. by rewrite ltrNl floor_le0 floorN lerNl oppr0. Qed.
 
-Lemma ceil_le0 x : x <= 0 -> Num.ceil x <= 0.
-Proof. by rewrite -ceil_ge_int. Qed.
+Lemma ceil_gt0 x : (0 < x) = (0 < Num.ceil x).
+Proof. by rewrite -ceil_gt_int. Qed.
 
-Lemma ceilN x : Num.ceil (- x) = - Num.floor x.
-Proof. by rewrite /Num.ceil opprK. Qed.
+Lemma ceil_le0 x : (x <= 0) = (Num.ceil x <= 0).
+Proof. by rewrite -Num.Theory.ceil_le_int. Qed.
 
 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 (ceil_ge _))// lerDl.
-by rewrite !ler0_norm ?ceil_le0// opprK intr1 ltW// lt_succ_floor.
+  by rewrite !gtr0_norm// -?ceil_gt0// (le_trans (Num.Theory.le_ceil _))// lerDl.
+by rewrite !ler0_norm -?ceil_le0// opprK intrD1 ltW// lt_succ_floor.
 Qed.
 
 End floor_ceil.
+
+#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed to `ceil_gt_int`")]
+Notation ceil_lt_int := ceil_gt_int (only parsing).

theories/lebesgue_integral.v

@@ -1434,7 +1434,7 @@ rewrite implyTb indicE mem_set ?mulr1; last first.
     rewrite ler_pdivrMr// (le_trans _ (ge_floor _))//.
     by rewrite -(@gez0_abs (floor _))// floor_ge0 mulr_ge0// ltW.
   rewrite ltr_pdivlMr// (lt_le_trans (lt_succ_floor _))//.
-  rewrite -[in leRHS]natr1 -intr1 lerD2r// -{1}(@gez0_abs (floor _))//.
+  rewrite -[in leRHS]natr1 -intrD1 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//.
@@ -1536,7 +1536,7 @@ have : fine (f x) < n%:R.
   rewrite -(@ler_nat R); apply: lt_le_trans.
   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 lt_succ_floor.
+  by rewrite intrD1 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.
@@ -1577,7 +1577,7 @@ case/cvg_ex => /= l; have [l0|l0] := leP 0%R l.
   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 (ceil _)) // ceil_ge0.
+  by rewrite -(@gez0_abs (ceil _)) // -ceil_ge0 (lt_le_trans _ l0).
 - move=> /cvgrPdist_lt/(_ _ ltr01)[n _].
   move=> /(_ (`|floor l|.+1 + n)%N)/(_ (leq_addl _ _)); apply/negP.
   rewrite approx_x -leNgt distrC (le_trans _ (lerB_normD _ _))//.
@@ -2340,7 +2340,8 @@ transitivity (\int[mu]_(x in D) limn (g^~ x)).
     near=> n; rewrite lee_fin -ler_pdivrMr//.
     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 natr_absz ger0_norm ?ceil_ge// -ceil_ge0// (lt_le_trans (ltrN10 _))//.
+    by rewrite divr_ge0// ?ltW.
   - rewrite lt0_mulye//; apply/cvgeNyPleNy; near=> M;
     have M0 : (M <= 0)%R by [].
     rewrite /g; case: (f x) fx0 => [r r0|//|_]; last first.
@@ -2349,8 +2350,8 @@ transitivity (\int[mu]_(x in D) limn (g^~ x)).
     near=> n; rewrite lee_fin -ler_ndivrMr//.
     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.
+    rewrite natr_absz ger0_norm ?ceil_ge// -ceil_ge0// (lt_le_trans (ltrN10 _))//.
+    by rewrite -mulrNN mulr_ge0// lerNr oppr0// ltW// invr_lt0.
   - rewrite -fx0 mule0 /g -fx0.
     under eq_fun do rewrite mule0/=. (*TODO: notation broken*)
     exact: cvg_cst.
@@ -2371,7 +2372,8 @@ rewrite -lee_pdivrMr//; last first.
 near: 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//.
+rewrite lee_fin natr_absz ger0_norm ?ceil_ge// -ceil_ge0//.
+rewrite (lt_le_trans (ltrN10 _))//.
 by rewrite mulr_ge0// ?invr_ge0//; exact/fine_ge0/integral_ge0.
 Unshelve. all: by end_near. Qed.
 
@@ -3437,7 +3439,7 @@ rewrite -[X in _ * X](@fineK _ (mu (E `&` D))); last first.
 rewrite lte_fin -ltr_pdivrMr.
   rewrite -natr1 natr_absz ger0_norm.
     by rewrite (le_lt_trans (ceil_ge _))// ltrDl.
-  by rewrite ceil_ge0// divr_ge0//; apply/le0R/measure_ge0; exact: measurableI.
+  by rewrite -ceil_ge0// (lt_le_trans (ltrN10 _))// divr_ge0.
 rewrite -lte_fin fineK.
   rewrite lt0e measure_ge0 andbT.
   suff: E `&` D = E by move=> ->; exact/eqP.
@@ -3685,7 +3687,8 @@ move=> mf; split=> [iDf0|Df0].
         - rewrite inE unitfE fine_eq0// abse_eq0 ft0/= fine_gt0//.
           by rewrite lt0e abse_ge0 abse_eq0 ft0 ltey.
         - by rewrite inE unitfE invr_eq0 pnatr_eq0 /= invr_gt0.
-      rewrite invrK /m -natr1 natr_absz ger0_norm ?ceil_ge0//.
+      rewrite invrK /m -natr1 natr_absz ger0_norm; last first.
+        by rewrite -ceil_ge0// (lt_le_trans (ltrN10 _)).
       rewrite (@le_trans _ _ ((fine `|f t|)^-1 + 1)%R) ?lerDl//.
       by rewrite lerD2r// ceil_ge.
     by split => //; apply: contraTN nft => /eqP ->; rewrite abse0 -ltNge.

theories/lebesgue_measure.v

@@ -1157,7 +1157,9 @@ rewrite predeqE => t; split => [/= [Dt ft]|].
   have [ft0|ft0] := leP 0%R (fine (f t)).
     exists `|ceil (fine (f t))|%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.
+    rewrite natr_absz ger0_norm; last first.
+      by rewrite -ceil_ge0 (lt_le_trans _ ft0).
+    by rewrite -(fineK ft) lee_fin ceil_ge.
   exists `|floor (fine (f t))|%N => //=; split => //; split.
     rewrite natr_absz ltr0_norm -?floor_lt0// EFinN.
     by rewrite -{2}(fineK ft) lee_fin mulrNz opprK ge_floor// ?num_real.
@@ -1417,7 +1419,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 // ?ceil_ge// ceil_gt0.
+by rewrite natr_absz gtr0_norm// ?ceil_ge// -ceil_gt0.
 Qed.
 
 End erealwithrays.
@@ -2440,8 +2442,9 @@ have finite_set_F i : finite_set (F i).
     - by move=> /= x [n Fni Bnx]; exists n => //; exists i.
   have {CFi Fir2} := le_trans MC (le_trans CFi Fir2).
   apply/negP; rewrite -ltNge lebesgue_measure_ball// lte_fin.
-  rewrite -(@natr1 _ `| _ |%N) natr_absz ger0_norm ?ceil_ge0// -ltr_pdivrMr//.
-  by rewrite -ltrBlDr (lt_le_trans _ (ceil_ge _))// ltrBlDr ltrDl.
+  rewrite -(@natr1 _ `| _ |%N) natr_absz ger0_norm; last first.
+    by rewrite -ceil_ge0// (lt_le_trans (ltrN10 _)).
+  by rewrite -ltr_pdivrMr// -ltrBlDr (lt_le_trans _ (ceil_ge _))// ltrBlDr ltrDl.
 have mur2_fin_num_ : mu (ball (0:R) (r%:num + 2))%R < +oo.
   by rewrite lebesgue_measure_ball// ltry.
 have FE : \sum_(n <oo) \esum_(i in F n) mu (closure (B i)) =

theories/lebesgue_stieltjes_measure.v

@@ -486,7 +486,7 @@ exists (fun k => `](- k%:R), k%:R]%classic).
   rewrite !natr_absz intr_norm intrD.
   suff: `|x| < `|(floor `|x|)%:~R + 1| by rewrite ltr_norml => /andP[-> /ltW->].
   rewrite [ltRHS]ger0_norm//.
-    by rewrite intr1 (le_lt_trans _ (lt_succ_floor _))// ?ler_norm.
+    by rewrite intrD1 (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.

theories/measure.v

@@ -2202,7 +2202,7 @@ Proof.
 move=> infA; apply/eqyP => r r0.
 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.
+  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.
   by move=> i /[!inE] /BA /mem_set iA; rewrite diracE iA.

theories/normedtype.v

@@ -255,11 +255,11 @@ Proof.
 apply/seteqP; split => // x _; have [x0|x0] := ltP 0%R x.
   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.
+  by rewrite -natr1 natr_absz -abszE gtz0_abs// -?ceil_gt0// ltr_pwDr.
 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.
+rewrite -natr1 natr_absz -abszE gez0_abs ?ltr_pwDr// -ceil_ge0 ltrNl opprK.
+by rewrite (le_lt_trans x0).
 Qed.
 
 Section lower_semicontinuous.
@@ -598,7 +598,7 @@ 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)) [ceil _]intEsign.
-by rewrite le_gtF ?expr0 ?mul1r ?lez_nat ?ceil_ge0//; near: n; apply: Foo.
+by rewrite le_gtF ?expr0 ?mul1r ?lez_nat -?ceil_ge0//; near: n; apply: Foo.
 Unshelve. all: by end_near. Qed.
 
 Section ecvg_infty_numField.
@@ -5973,7 +5973,7 @@ exists j; split => //.
 Qed.
 
 Lemma vitali_lemma_infinite_cover : { D : set I | [/\ countable D,
-  D `<=` V, trivIset D (closure\o B) &
+  D `<=` V, trivIset D (closure \o B) &
   cover V (closure \o B) `<=` cover D (closure \o scale_ball 5%:R \o B)] }.
 Proof.
 have [D [cD DV tD maxD]] := vitali_lemma_infinite.

theories/real_interval.v

@@ -177,7 +177,7 @@ 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// intr1 lt_succ_floor.
+by rewrite -natr1 natr_absz ger0_norm ?floor_ge0 1?ltW// intrD1 lt_succ_floor.
 Qed.
 
 Lemma itv_o_inftyEbigcup x :
@@ -344,7 +344,7 @@ move fxE : (f x) => fx; case: fx fxE => [fx fxE gxE|fxoo gxE _|//]; last first.
 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 rewrite intr1 ltW// lt_succ_floor.
+- by rewrite intrD1 ltW// lt_succ_floor.
 - by rewrite posrE// ltr_pwDr// ler0z floor_ge0 invr_ge0 ltW.
 - by rewrite posrE invr_gt0.
 Qed.
@@ -367,7 +367,7 @@ apply/ler_addgt0Pl => e e_gt0; rewrite -lerBlDl ltW//.
 have := rx `|floor e^-1|%N I; rewrite /= in_itv => /andP[/le_lt_trans->]//.
 rewrite lerD2l lerN2 -lef_pV2 ?invrK//; last by rewrite posrE.
 rewrite -natr1 natr_absz ger0_norm ?floor_ge0 ?invr_ge0 1?ltW//.
-by rewrite intr1 lt_succ_floor.
+by rewrite intrD1 lt_succ_floor.
 Qed.
 
 Lemma itv_bnd_open_bigcup (R : realType) b (r s : R) :
@@ -381,7 +381,7 @@ 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.
-    by rewrite ceil_ge0// invr_ge0 subr_ge0 ltW.
+    by rewrite -ceil_ge0 (lt_le_trans (ltrN10 R))// invr_ge0 subr_ge0 ltW.
   by rewrite (@le_trans _ _ (ceil (s - x)^-1)%:~R)// ?lerDl// ceil_ge.
 - by rewrite inE unitfE ltr0n andbT pnatr_eq0.
 - by rewrite inE invr_gt0 subr_gt0 xs andbT unitfE invr_eq0 subr_eq0 gt_eqF.
@@ -405,7 +405,8 @@ Proof.
 apply/seteqP; split=> y; rewrite /= !in_itv/= andbT; last first.
   by move=> [k _ /=]; move: b => [|] /=; rewrite in_itv/= => /andP[//] /ltW.
 move=> xy; exists `|ceil (y - x)|%N => //=; rewrite in_itv/= xy/= -lerBlDl.
-rewrite !natr_absz/= ger0_norm ?ceil_ge0 ?subr_ge0 ?ceil_ge//.
+rewrite !natr_absz/= ger0_norm -?ceil_ge0 ?ceil_ge//.
+rewrite (lt_le_trans (ltrN10 R))// subr_ge0.
 by case: b xy => //= /ltW.
 Qed.
 
@@ -426,7 +427,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 ?intr1 ?lt_succ_floor// ler0z addr_ge0// floor_ge0.
+  by rewrite [ltRHS]ger0_norm ?intrD1 ?lt_succ_floor// ler0z addr_ge0// floor_ge0.
 case: b => /=.
 - by move/ltW; rewrite ler_norml => /andP[-> ->].
 - by rewrite ltr_norml => /andP[-> /ltW->].

theories/realfun.v

@@ -186,7 +186,7 @@ exists (fun n => sval (cid (He (PosNum (invn n))))).
   rewrite distrC (lt_le_trans xpt)// -(@invrK _ r) lef_pV2 ?posrE ?invr_gt0//.
   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.
+  by rewrite natr_absz gtr0_norm -?ceil_gt0 ?invr_gt0// ceil_ge.
 move=> /cvgrPdist_lt/(_ e%:num (ltac:(by [])))[] n _ /(_ _ (leqnn _)).
 rewrite /sval/=; case: cid => // x [px xpn].
 by rewrite leNgt distrC => /negP.
@@ -236,7 +236,7 @@ have y_p : y_ n @[n --> \oo] --> p.
   near: t.
   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 rewrite ger0_norm -?ceil_ge0// (lt_le_trans (ltrN10 _))// 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).
 near \oo => n.

theories/reals.v

@@ -465,7 +465,7 @@ Lemma RfloorE x : Rfloor x = (floor x)%:~R.
 Proof. by []. Qed.
 
 Lemma mem_rg1_floor x : (range1 (floor x)%:~R) x.
-Proof. by rewrite /range1 /mkset intr1 ge_floor lt_succ_floor. Qed.
+Proof. by rewrite /range1 /mkset intrD1 ge_floor lt_succ_floor. Qed.
 
 Lemma mem_rg1_Rfloor x : (range1 (Rfloor x)) x.
 Proof. exact: mem_rg1_floor. Qed.
@@ -496,7 +496,7 @@ Proof. by rewrite /range1/mkset lexx /= ltrDl ltr01. Qed.
 Lemma range1zP (m : int) x : Rfloor x = m%:~R <-> (range1 m%:~R) x.
 Proof.
 split=> [<-|h]; first exact/mem_rg1_Rfloor.
-by congr intmul; apply/floor_def; rewrite -intr1.
+by congr intmul; apply/floor_def; rewrite -intrD1.
 Qed.
 
 Lemma Rfloor_natz (z : int) : Rfloor z%:~R = z%:~R :> R.
@@ -532,7 +532,7 @@ 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// invr_ge0 subr_ge0 ltW.
-by rewrite intr1 lt_succ_floor.
+by rewrite intrD1 lt_succ_floor.
 Qed.
 
 End FloorTheory.

theories/sequences.v

@@ -1277,7 +1277,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 `|floor x|.+1 => // m; rewrite /mkset -(@ler_nat R).
 move/lt_le_trans => -> //; rewrite (lt_le_trans (lt_succ_floor x))//.
-by rewrite -intr1 -natr1 lerD2r -(@gez0_abs (floor x)) ?floor_ge0// ltW.
+by rewrite -intrD1 -natr1 lerD2r -(@gez0_abs (floor x)) ?floor_ge0// ltW.
 Unshelve. all: by end_near. Qed.
 
 End exponential_series_cvg.