try to make floor a notation (wip)

CHANGELOG_UNRELEASED.md

@@ -7,10 +7,14 @@
 - in `reals.v`:
   + lemma `mem_rg1_floor`
 
+- in `mathcomp_extra.v`:
+  + lemmas `intr1`, `int1r`
+
 ### Changed
 
 - in `reals.v`:
-  + definitions `Rceil`, `ceil`, `Rfloor`, `floor`
+  + definition `floor` now a notation (in `real_scope`)
+  + definitions `Rceil`, `ceil`, `Rfloor`
 
 ### Renamed
 
@@ -20,6 +24,10 @@
 
 ### Removed
 
+- in `reals.v`:
+  + `lt_succ_floor` renamed to `__deprecated__lt_succ_floor`
+    (use `lt_succ_floor` from MathComp instead)
+
 ### Infrastructure
 
 ### Misc

classical/mathcomp_extra.v

@@ -374,3 +374,9 @@ by elim: p => //= p <-;
 Qed.
 
 End positive.
+
+Lemma intr1 {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.
+Proof. by rewrite intrD. Qed.

theories/altreals/realsum.v

@@ -4,7 +4,7 @@
 (* Copyright (c) - 2016--2018 - Polytechnique                           *)
 
 (* -------------------------------------------------------------------- *)
-From mathcomp Require Import all_ssreflect all_algebra.
+From mathcomp Require Import all_ssreflect all_algebra archimedean.
 From mathcomp.classical Require Import boolp.
 Require Import xfinmap ereal reals discrete realseq.
 From mathcomp.classical Require Import classical_sets functions mathcomp_extra.
@@ -142,15 +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|)|%N; exists j; rewrite inE.
+  pose j := `|(floor (1 / `|f x|))%real|%N; exists j; rewrite inE.
   rewrite ltr_pdivrMr ?ltr0z // -ltr_pdivrMl ?normr_gt0 //.
   rewrite mulr1 /j div1r -addn1 /= PoszD intrD mulr1z.
-  by rewrite gez0_abs ?floor_ge0 ?invr_ge0 ?normr_ge0 // lt_succ_floor.
+  rewrite gez0_abs ?floor_ge0 ?invr_ge0 ?normr_ge0//.
+  by rewrite intr1 lt_succ_floor// num_real.
 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)|.+1.
-pose K := (`|floor M|.+1 * i.+1)%N; move/(_ K)/asboolP/exists_asboolP.
+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=> 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.
@@ -160,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 _]gez0_abs // floor_ge0.
+by rewrite natrD /= mulr1n pmulrn -{1}[(floor _)%real]gez0_abs // floor_ge0.
 Qed.
 
 End SummableCountable.
@@ -1201,9 +1202,8 @@ Qed.
 
 Lemma sum_seq1 S x : (forall y, S y != 0 -> x == y) -> sum S = S x.
 Proof.
-move=> domS; rewrite (sum_finseq (r := [:: x])) //.
-  by move=> y; rewrite !inE => /domS /eqP->.
-by rewrite big_seq1.
+move=> domS; rewrite (sum_finseq (r := [:: x])) ?big_seq1//.
+by move=> y; rewrite !inE => /domS /eqP->.
 Qed.
 
 End SumTheory.

theories/ereal.v

@@ -1402,21 +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) \is a Znat.
+    have /ZnatP[N Nfloor] : (floor (Num.max d 0%R))%real \is a Znat.
       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.
-    by apply; rewrite (lt_le_trans (reals.lt_succ_floor _))// Nfloor natr1 ler_nat.
-  have /ZnatP [N Nfloor] : floor (Num.max (- d)%R 0%R) \is a Znat.
+    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.
   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.
-  by apply; rewrite (lt_le_trans (reals.lt_succ_floor _))// Nfloor natr1 ler_nat.
-have /ZnatP[N Nfloor] : floor (d%:num^-1) \is a Num.nat.
+  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.
 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.
-by rewrite (lt_le_trans (reals.lt_succ_floor _))// Nfloor lerD// ler_nat.
+rewrite (lt_le_trans (lt_succ_floor _)) ?num_real// Nfloor.
+by rewrite -intr1 lerD// ler_nat.
 Qed.

theories/lebesgue_integral.v

@@ -1287,11 +1287,11 @@ Lemma bigsetU_dyadic_itv n : `[n%:R, n.+1%:R[%classic =
   \big[setU/set0]_(n * 2 ^ n.+1 <= k < n.+1 * 2 ^ n.+1) [set` I n.+1 k].
 Proof.
 rewrite predeqE => r; split => [/= /[!in_itv]/= /andP[nr rn1]|].
-- rewrite -bigcup_seq /=; exists `|reals.floor (r * 2 ^+ n.+1)|%N.
+- rewrite -bigcup_seq /=; exists `|(floor (r * 2 ^+ n.+1))%real|%N.
     rewrite /= mem_index_iota; apply/andP; split.
-      rewrite -ltez_nat gez0_abs ?reals.floor_ge0; last first.
+      rewrite -ltez_nat gez0_abs ?floor_ge0; last first.
         by rewrite mulr_ge0// (le_trans _ nr).
-      apply: (@le_trans _ _ (reals.floor (n * 2 ^ n.+1)%:R)); last first.
+      apply: (@le_trans _ _ (floor (n * 2 ^ n.+1)%:R)%real); last first.
         by apply: le_floor; rewrite natrM natrX ler_pM2r.
       by rewrite -floor_ge_int.
     rewrite -ltz_nat gez0_abs; last first.
@@ -1300,9 +1300,9 @@ rewrite predeqE => r; split => [/= /[!in_itv]/= /andP[nr rn1]|].
     by rewrite PoszM intrM -natrX ltr_pM2r.
   rewrite /= in_itv /=; apply/andP; split.
     rewrite ler_pdivrMr// (le_trans _ (reals.floor_le _))//.
-    by rewrite -(@gez0_abs (reals.floor _))// floor_ge0 mulr_ge0// (le_trans _ nr).
-  rewrite ltr_pdivlMr// (lt_le_trans (reals.lt_succ_floor _))//.
-  rewrite -[in leRHS]natr1 lerD2r// -(@gez0_abs (reals.floor _))// floor_ge0.
+    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.
   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.
@@ -1430,7 +1430,7 @@ rewrite pnatr_eq0 => /eqP.
 have [//|] := boolP (x \in B n).
 rewrite notin_setE /B /setI /= => /not_andP[] // /negP.
 rewrite -ltNge => fxn _.
-have K : (`|reals.floor (fine (f x) * 2 ^+ n)| < n * 2 ^ n)%N.
+have K : (`|(floor (fine (f x) * 2 ^+ n))%real| < n * 2 ^ n)%N.
   rewrite -ltz_nat gez0_abs; last by rewrite reals.floor_ge0 mulr_ge0// ltW.
   rewrite -(@ltr_int R); rewrite (le_lt_trans (reals.floor_le _))// PoszM intrM.
   by rewrite -natrX ltr_pM2r// -lte_fin (fineK fxfin).
@@ -1439,9 +1439,10 @@ rewrite implyTb indicE mem_set ?mulr1; last first.
   rewrite /A K /= inE; split=> //=; exists (fine (f x)); last by rewrite fineK.
   rewrite in_itv /=; apply/andP; split.
     rewrite ler_pdivrMr// (le_trans _ (reals.floor_le _))//.
-    by rewrite -(@gez0_abs (reals.floor _))// reals.floor_ge0 mulr_ge0// ltW.
-  rewrite ltr_pdivlMr// (lt_le_trans (reals.lt_succ_floor _))// -[in leRHS]natr1.
-  by rewrite lerD2r// -{1}(@gez0_abs (reals.floor _))// reals.floor_ge0// mulr_ge0// ltW.
+    by rewrite -(@gez0_abs (floor _)%real)// reals.floor_ge0 mulr_ge0// ltW.
+  rewrite ltr_pdivlMr// (lt_le_trans (lt_succ_floor _)) ?num_real//.
+  rewrite -[in leRHS]natr1 -intr1 lerD2r// -{1}(@gez0_abs (floor _)%real)//.
+  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//.
 apply/orP; right; apply/ltW; near: n.
@@ -1538,11 +1539,11 @@ near=> n.
 have mn : (m <= n)%N by near: n; exists m.
 have : fine (f x) < n%:R.
   near: n.
-  exists `|reals.floor (fine (f x))|.+1%N => //= p /=.
+  exists `|(floor (fine (f x)))%real|.+1%N => //= p /=.
   rewrite -(@ler_nat R); apply: lt_le_trans.
-  rewrite -natr1 (_ : `| _ |%:R  = (reals.floor (fine (f x)))%:~R); last first.
-    by rewrite -[in RHS](@gez0_abs (reals.floor _))// reals.floor_ge0//; exact/fine_ge0/f0.
-  by rewrite reals.lt_succ_floor.
+  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.
 rewrite -lte_fin (fineK fxfin) => fxn.
 have [approx_nx0|[k [/andP[k0 kn2n] ? ->]]] := f_ub_approx fxn.
   by have := Hm _ mn; rewrite approx_nx0.
@@ -1585,14 +1586,14 @@ case/cvg_ex => /= l; have [l0|l0] := leP 0%R l.
   rewrite natrD lerD// ?ler1n// ger0_norm // (le_trans (ceil_ge _)) //.
   by rewrite -(@gez0_abs (reals.ceil _)) // ceil_ge0.
 - move/cvgrPdist_lt => /(_ _ ltr01) -[n _].
-  move=> /(_ (`|reals.floor l|.+1 + n)%N) /= /(_ (leq_addl _ _)).
+  move=> /(_ (`|(floor l)%real|.+1 + n)%N) /= /(_ (leq_addl _ _)).
   rewrite approx_x.
   apply/negP; rewrite -leNgt distrC (le_trans _ (lerB_normD _ _)) //.
   rewrite normrN lerBrDl addSnnS [leRHS]ger0_norm ?ler0n//.
   rewrite natrD lerD// ?ler1n// ler0_norm //; last by rewrite ltW.
-  rewrite (@le_trans _ _ (- reals.floor l)%:~R) //.
+  rewrite (@le_trans _ _ (- floor l)%real%:~R) //.
     by rewrite mulrNz lerNl opprK reals.floor_le.
-  by rewrite -(@lez0_abs (reals.floor _)) // reals.floor_le0 // ltW.
+  by rewrite -(@lez0_abs (floor _)%real)// floor_le0 // ltW.
 Qed.
 
 Lemma ecvg_approx (f0 : forall x, D x -> (0 <= f x)%E) x :

theories/lebesgue_measure.v

@@ -967,7 +967,7 @@ rewrite predeqE => t; split => [/= [Dt ft]|].
     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.
-  exists `|floor (fine (f t))|%N => //=; split => //; split.
+  exists `|(floor (fine (f t)))%real|%N => //=; split => //; split.
     rewrite natr_absz ltr0_norm ?floor_lt0// EFinN.
     by rewrite -{2}(fineK ft) lee_fin mulrNz opprK floor_le.
   by rewrite -(fineK ft)// lee_fin (le_trans (ltW ft0)).
@@ -1212,7 +1212,7 @@ Lemma eset1Ny :
 Proof.
 rewrite eqEsubset; split=> [_ -> i _ |]; first by rewrite /= in_itv /= ltNyr.
 move=> [r|/(_ O Logic.I)|]//.
-move=> /(_ `|floor r|%N Logic.I); rewrite /= in_itv/= ltNge.
+move=> /(_ `|(floor r)%real|%N Logic.I); rewrite /= in_itv/= ltNge.
 rewrite lee_fin; have [r0|r0] := leP 0%R r.
   by rewrite (le_trans _ r0) // lerNl oppr0 ler0n.
 rewrite lerNl -abszN natr_absz gtr0_norm; last first.

theories/lebesgue_stieltjes_measure.v

@@ -1,6 +1,6 @@
 (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
 From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval.
-From mathcomp Require Import finmap fingroup perm rat.
+From mathcomp Require Import finmap fingroup perm rat archimedean.
 From HB Require Import structures.
 From mathcomp.classical Require Import mathcomp_extra boolp classical_sets.
 From mathcomp.classical Require Import functions fsbigop cardinality.
@@ -480,11 +480,11 @@ Lemma wlength_sigma_finite (f : R -> R) :
 Proof.
 exists (fun k => `](- k%:R), k%:R]%classic).
   apply/esym; rewrite -subTset => /= x _ /=.
-  exists `|(floor `|x|%R + 1)%R|%N; rewrite //= in_itv/=.
+  exists `|((floor `|x|%R)%real + 1)%R|%N; rewrite //= in_itv/=.
   rewrite !natr_absz intr_norm intrD.
-  suff: `|x| < `|(floor `|x|)%:~R + 1| by rewrite ltr_norml => /andP[-> /ltW->].
+  suff: `|x| < `|(floor `|x|)%real%:~R + 1| by rewrite ltr_norml => /andP[-> /ltW->].
   rewrite [ltRHS]ger0_norm//.
-    by rewrite (le_lt_trans _ (lt_succ_floor _))// ?ler_norm.
+    by rewrite intr1 (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/normedtype.v

@@ -4919,7 +4919,7 @@ Lemma compact_bounded (K : realType) (V : normedModType K) (A : set V) :
 Proof.
 rewrite compact_cover => Aco.
 have covA : A `<=` \bigcup_(n : int) [set p | `|p| < n%:~R].
-  by move=> p _; exists (reals.floor `|p| + 1) => //; rewrite rmorphD/= reals.lt_succ_floor.
+  by move=> p _; exists ((floor `|p|)%real + 1) => //=; rewrite lt_succ_floor.
 have /Aco [] := covA.
   move=> n _; rewrite openE => p; rewrite /= -subr_gt0 => ltpn.
   apply/nbhs_ballP; exists (n%:~R - `|p|) => // q.
@@ -5763,13 +5763,13 @@ Notation r_gt0 := vitali_collection_partition_ub_gt0.
 Lemma ex_vitali_collection_partition i :
   V i -> exists n, vitali_collection_partition n i.
 Proof.
-move=> Vi; pose f := reals.floor (r / (radius (B i))%:num).
+move=> Vi; pose f := (floor (r / (radius (B i))%:num))%real.
 have f_ge0 : 0 <= f by rewrite floor_ge0// divr_ge0// ltW// (r_gt0 Vi).
 have [m /andP[mf fm]] := leq_ltn_expn `|f|.-1.
 exists m; split => //; apply/andP; split => [{mf}|{fm}].
   rewrite -(@ler_nat R) in fm.
   rewrite ltr_pdivrMr// mulrC -ltr_pdivrMr// (lt_le_trans _ fm)//.
-  rewrite (lt_le_trans (reals.lt_succ_floor _))//= -/f -natr1 lerD2r//.
+  rewrite (lt_le_trans (lt_succ_floor _))//= -/f intrD -natr1 lerD2r//.
   have [<-|f0] := eqVneq 0 f; first by rewrite /= ler0n.
   rewrite prednK//; last by rewrite absz_gt0 eq_sym.
   by rewrite natr_absz// ger0_norm.

theories/real_interval.v

@@ -1,6 +1,6 @@
 (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
 From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval.
-From mathcomp Require Import finmap fingroup perm rat.
+From mathcomp Require Import fingroup perm rat archimedean finmap.
 From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
 From mathcomp Require Export set_interval.
 From HB Require Import structures.
@@ -173,10 +173,11 @@ Lemma itv_bnd_inftyEbigcup b x : [set` Interval (BSide b x) +oo%O] =
 Proof.
 rewrite predeqE => y; split=> /=; last first.
   by move=> [n _]/=; rewrite in_itv => /andP[xy yn]; rewrite in_itv /= xy.
-rewrite in_itv /= andbT => xy; exists `|floor y|%N.+1 => //=.
+rewrite in_itv /= andbT => xy; exists `|(floor y)%real|%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// lt_succ_floor.
+rewrite -natr1 natr_absz ger0_norm ?floor_ge0 1?ltW//.
+by rewrite intr1 lt_succ_floor// num_real.
 Qed.
 
 Lemma itv_o_inftyEbigcup x :
@@ -340,10 +341,10 @@ move gxE : (g x) => gx; case: gx gxE => [gx| |gxoo fxoo]; last 2 first.
   - by exists 0%N => //; rewrite /E/= gxoo addey// ?leey// -ltNye.
 move fxE : (f x) => fx; case: fx fxE => [fx fxE gxE|fxoo gxE _|//]; last first.
   by exists 0%N => //; rewrite /E/= fxoo gxE// addye// leey.
-rewrite lte_fin -subr_gt0 => fgx; exists `|floor (fx - gx)^-1%R|%N => //.
+rewrite lte_fin -subr_gt0 => fgx; exists `|(floor (fx - gx)^-1)%real|%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 apply/ltW; rewrite lt_succ_floor.
+- by rewrite intr1 ltW// lt_succ_floor// num_real.
 - by rewrite posrE// ltr_pwDr// ler0z floor_ge0 invr_ge0 ltW.
 - by rewrite posrE invr_gt0.
 Qed.
@@ -363,9 +364,10 @@ apply/seteqP; split=> [x ->|].
   by move=> i _/=; rewrite in_itv/= lexx ltrBlDr ltrDl invr_gt0 ltr0n.
 move=> x rx; apply/esym/eqP; rewrite eq_le (itvP (rx 0%N _))// andbT.
 apply/ler_addgt0Pl => e e_gt0; rewrite -lerBlDl ltW//.
-have := rx `|floor e^-1%R|%N I; rewrite /= in_itv => /andP[/le_lt_trans->]//.
+have := rx `|(floor e^-1)%real|%N I; rewrite /= in_itv => /andP[/le_lt_trans->]//.
 rewrite lerD2l lerN2 -lef_pV2 ?invrK//; last by rewrite posrE.
-by rewrite -natr1 natr_absz ger0_norm ?floor_ge0 ?invr_ge0 1?ltW// lt_succ_floor.
+rewrite -natr1 natr_absz ger0_norm ?floor_ge0 ?invr_ge0 1?ltW//.
+by rewrite intr1 lt_succ_floor// num_real.
 Qed.
 
 Lemma itv_bnd_open_bigcup (R : realType) b (r s : R) :
@@ -421,10 +423,10 @@ Qed.
 Lemma bigcup_itvT {R : realType} b :
   \bigcup_i [set` Interval (BSide b (- i%:R)) (BRight i%:R)] = [set: R].
 Proof.
-rewrite -subTset => x _ /=; exists `|(floor `|x| + 1)%R|%N => //=.
+rewrite -subTset => x _ /=; exists `|((floor `|x|)%real + 1)%R|%N => //=.
 rewrite in_itv/= !natr_absz intr_norm intrD.
-have : `|x| < `|(floor `|x|)%:~R + 1|.
-  by rewrite [ltRHS]ger0_norm ?lt_succ_floor// addr_ge0// ler0z floor_ge0.
+have : `|x| < `|(floor `|x|)%real%:~R + 1|.
+  by rewrite [ltRHS]ger0_norm ?intr1 ?lt_succ_floor// ler0z addr_ge0// floor_ge0.
 case: b => /=.
 - by move/ltW; rewrite ler_norml => /andP[-> ->].
 - by rewrite ltr_norml => /andP[-> /ltW->].