ceil as a notation, deprecate floor_le

CHANGELOG_UNRELEASED.md

@@ -14,14 +14,18 @@
 
 - in `reals.v`:
   + definition `floor` now a notation (in `real_scope`)
-  + definitions `Rceil`, `ceil`, `Rfloor`
+  + definition `ceil` now a notation (in `real_scope`)
+  + definitions `Rceil`, `Rfloor`
 
 ### Renamed
 
 ### Generalized
 
 ### Deprecated
 
+- in `reals.v`:
+  + `floor_le` -> `__deprecated__floor_le` (use `ge_floor` instead)
+
 ### Removed
 
 - in `reals.v`:

theories/lebesgue_integral.v

@@ -1296,10 +1296,10 @@ rewrite predeqE => r; split => [/= /[!in_itv]/= /andP[nr rn1]|].
       by rewrite -floor_ge_int.
     rewrite -ltz_nat gez0_abs; last first.
       by rewrite floor_ge0 mulr_ge0// (le_trans _ nr).
-    rewrite -(@ltr_int R) (le_lt_trans (reals.floor_le _))//.
+    rewrite -(@ltr_int R) (le_lt_trans (ge_floor _)) ?num_real//.
     by rewrite PoszM intrM -natrX ltr_pM2r.
   rewrite /= in_itv /=; apply/andP; split.
-    rewrite ler_pdivrMr// (le_trans _ (reals.floor_le _))//.
+    rewrite ler_pdivrMr// (le_trans _ (ge_floor _)) ?num_real//.
     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.
@@ -1432,13 +1432,13 @@ rewrite notin_setE /B /setI /= => /not_andP[] // /negP.
 rewrite -ltNge => fxn _.
 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.
+  rewrite -(@ltr_int R); rewrite (le_lt_trans (ge_floor _)) ?num_real// PoszM intrM.
   by rewrite -natrX ltr_pM2r// -lte_fin (fineK fxfin).
 have /[!mem_index_enum]/(_ isT) := An0 (Ordinal K).
 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 _))//.
+    rewrite ler_pdivrMr// (le_trans _ (ge_floor _)) ?num_real//.
     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)//.
@@ -1579,20 +1579,20 @@ move=> Dx fxoo; have approx_x n : approx n x = n%:R.
   by rewrite fgen_A0 // ?mulr0 // fxoo leey.
 case/cvg_ex => /= l; have [l0|l0] := leP 0%R l.
 - move=> /cvgrPdist_lt/(_ _ ltr01) -[n _].
-  move=> /(_ (`|reals.ceil l|.+1 + n)%N) /= /(_ (leq_addl _ _)).
+  move=> /(_ (`|(ceil 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// ger0_norm // (le_trans (ceil_ge _)) //.
-  by rewrite -(@gez0_abs (reals.ceil _)) // ceil_ge0.
+  by rewrite -(@gez0_abs (ceil _)%real) // ceil_ge0.
 - move/cvgrPdist_lt => /(_ _ ltr01) -[n _].
   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 _ _ (- floor l)%real%:~R) //.
-    by rewrite mulrNz lerNl opprK reals.floor_le.
+    by rewrite mulrNz lerNl opprK ge_floor.
   by rewrite -(@lez0_abs (floor _)%real)// floor_le0 // ltW.
 Qed.
 
@@ -2347,7 +2347,7 @@ transitivity (\int[mu]_(x in D) limn (g^~ x)).
       exists 1%N => // m /= m0.
       by rewrite mulry gtr0_sg// ?mul1e ?leey// ltr0n.
     near=> n; rewrite lee_fin -ler_pdivrMr//.
-    near: n; exists `|reals.ceil (M / r)|%N => // m /=.
+    near: n; exists `|(ceil (M / r))%real|%N => // m /=.
     rewrite -(ler_nat R); apply: le_trans.
     by rewrite natr_absz ger0_norm ?ceil_ge// ceil_ge0// divr_ge0// ?ltW.
   - rewrite lt0_mulye//; apply/cvgeNyPleNy; near=> M;
@@ -2356,7 +2356,7 @@ transitivity (\int[mu]_(x in D) limn (g^~ x)).
       exists 1%N => // m /= m0.
       by rewrite mulrNy gtr0_sg// ?ltr0n// mul1e ?leNye.
     near=> n; rewrite lee_fin -ler_ndivrMr//.
-    near: n; exists `|reals.ceil (M / r)|%N => // m /=.
+    near: n; exists `|(ceil (M / r))%real|%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.
@@ -2378,7 +2378,7 @@ rewrite -(@fineK _ (\int[mu]_(x in D) f x)); last first.
 rewrite -lee_pdivr_mulr//; last first.
   by move: if_gt0 ifoo; case: (\int[mu]_(x in D) f x).
 near: n.
-exists `|reals.ceil (M * (fine (\int[mu]_(x in D) f x))^-1)|%N => //.
+exists `|(ceil (M * (fine (\int[mu]_(x in D) f x))^-1))%real|%N => //.
 move=> n /=; rewrite -(@ler_nat R) -lee_fin; apply: le_trans.
 rewrite lee_fin natr_absz ger0_norm ?ceil_ge// ceil_ge0//.
 by rewrite mulr_ge0// ?invr_ge0//; exact/fine_ge0/integral_ge0.
@@ -2609,7 +2609,7 @@ Proof.
 move=> muD0; pose g : (T -> \bar R)^nat := fun n => cst n%:R%:E.
 have <- : (fun t => limn (g^~ t)) = cst +oo.
   rewrite funeqE => t; apply/cvg_lim => //=.
-  apply/cvgeryP/cvgryPge => M; exists `|reals.ceil M|%N => //= m.
+  apply/cvgeryP/cvgryPge => M; exists `|(ceil M)%real|%N => //= m.
   rewrite /= -(ler_nat R); apply: le_trans.
   by rewrite (le_trans (ceil_ge _))// natr_absz ler_int ler_norm.
 rewrite monotone_convergence //.
@@ -2618,7 +2618,7 @@ rewrite monotone_convergence //.
   have [muDoo|muDoo] := ltP (mu D) +oo; last first.
     exists 1%N => // m /= m0; move: muDoo; rewrite leye_eq => /eqP ->.
     by rewrite mulry gtr0_sg ?mul1e ?leey// ltr0n.
-  exists `|reals.ceil (M / fine (mu D))|%N => // m /=.
+  exists `|(ceil (M / fine (mu D)))%real|%N => // m /=.
   rewrite -(ler_nat R) => MDm; rewrite -(@fineK _ (mu D)) ?ge0_fin_numE//.
   rewrite -lee_pdivr_mulr; last by rewrite fine_gt0// lt0e muD0 measure_ge0.
   rewrite lee_fin (le_trans _ MDm)//.
@@ -3439,7 +3439,7 @@ have [M M0 muM] : exists2 M, (0 <= M)%R &
 apply/eqP/negPn/negP => /eqP muED0; move/not_forallP : muM; apply.
 have [muEDoo|] := ltP (mu (E `&` D)) +oo; last first.
   by rewrite leye_eq => /eqP ->; exists 1%N; rewrite mul1e leye_eq.
-exists `|reals.ceil (M * (fine (mu (E `&` D)))^-1)|%N.+1.
+exists `|(ceil (M * (fine (mu (E `&` D)))^-1))%real|%N.+1.
 apply/negP; rewrite -ltNge.
 rewrite -[X in _ * X](@fineK _ (mu (E `&` D))); last first.
   by rewrite fin_numElt muEDoo (lt_le_trans _ (measure_ge0 _ _)).
@@ -3687,7 +3687,7 @@ move=> mf; split=> [iDf0|Df0].
     rewrite predeqE => t; split=> [[Dt ft0]|[n _ /= [Dt nft]]].
       have [ftoo|ftoo] := eqVneq `|f t| +oo.
         by exists 0%N => //; split => //=; rewrite ftoo /= leey.
-      pose m := `|reals.ceil (fine `|f t|)^-1|%N.
+      pose m := `|(ceil (fine `|f t|)^-1)%real|%N.
       have ftfin : `|f t|%E \is a fin_num by rewrite ge0_fin_numE// ltey.
       exists m => //; split => //=.
       rewrite -(@fineK _ `|f t|) // lee_fin -ler_pV2; last 2 first.
@@ -6457,7 +6457,7 @@ move=> Ef; have {Ef} : mu.-negligible (E `&` [set x | 0 < f^* x]).
   near \oo => m; exists m => //=.
   rewrite -(@fineK _ (f^* x)) ?gt0_fin_numE ?ltey// lte_fin.
   rewrite invf_plt ?posrE//; last by rewrite fine_gt0// ltey fx0.
-  set r := _^-1; rewrite (@le_lt_trans _ _ `|reals.ceil r|.+1%:R)//.
+  set r := _^-1; rewrite (@le_lt_trans _ _ `|(ceil r)%real|.+1%:R)//.
     by rewrite (le_trans _ (abs_ceil_ge _))// ler_norm.
   by rewrite ltr_nat ltnS; near: m; exact: nbhs_infty_gt.
 apply: negligibleS => z /= /not_implyP[Ez H]; split => //.
@@ -6659,14 +6659,14 @@ have fE y k r : (ball 0%R k.+1%:R) y -> (r < 1)%R ->
   rewrite (le_trans (ltW yk1))// -lerBlDr opprK -lerBrDl.
   rewrite -natrB//; last by rewrite -addnn addSnnS ltn_addl.
   by rewrite -addnn addnK ler1n.
-have := h `|reals.ceil x|.+1%N Logic.I.
-have Bxx : B `|reals.ceil x|.+1 x.
+have := h `|(ceil x)%real|.+1%N Logic.I.
+have Bxx : B `|(ceil x)%real|.+1 x.
   rewrite /B /ball/= sub0r normrN (le_lt_trans (abs_ceil_ge _))// ltr_nat.
   by rewrite -addnn addSnnS ltn_addl.
 move=> /(_ Bxx)/fine_cvgP[davg_fk_fin_num davg_fk0].
 have f_fk_ceil : \forall t \near 0^'+,
   \int[mu]_(y in ball x t) `|(f y)%:E - (f x)%:E| =
-  \int[mu]_(y in ball x t) `|fk `|reals.ceil x|.+1 y - fk `|reals.ceil x|.+1 x|%:E.
+  \int[mu]_(y in ball x t) `|fk `|(ceil x)%real|.+1 y - fk `|(ceil x)%real|.+1 x|%:E.
   near=> t.
   apply: eq_integral => /= y /[1!inE] xty.
   rewrite -(fE x _ t)//; last first.

theories/lebesgue_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 mathcomp Require Import mathcomp_extra boolp classical_sets functions.
 From mathcomp Require Import cardinality fsbigop.
 Require Import reals ereal signed topology numfun normedtype function_spaces.
@@ -964,12 +964,12 @@ rewrite [X in measurable X](_ : _ =
                           exact: emeasurable_fun_infty_c].
 rewrite predeqE => t; split => [/= [Dt ft]|].
   have [ft0|ft0] := leP 0%R (fine (f t)).
-    exists `|ceil (fine (f t))|%N => //=; split => //; split.
+    exists `|(ceil (fine (f t)))%real|%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)))%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 -{2}(fineK ft) lee_fin mulrNz opprK ge_floor// ?num_real.
   by rewrite -(fineK ft)// lee_fin (le_trans (ltW ft0)).
 move=> [n _] [/= Dt [nft fnt]]; split => //; rewrite fin_numElt.
 by rewrite (lt_le_trans _ nft) ?ltNyr//= (le_lt_trans fnt)// ltry.
@@ -1217,13 +1217,13 @@ 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.
   by rewrite ltrNr oppr0 floor_lt0.
-by rewrite mulrNz lerNl opprK floor_le.
+by rewrite mulrNz lerNl opprK ge_floor.
 Qed.
 
 Lemma eset1y : [set +oo] = \bigcap_k `]k%:R%:E, +oo[%classic :> set (\bar R).
 Proof.
 rewrite eqEsubset; split=> [_ -> i _/=|]; first by rewrite in_itv /= ltry.
-move=> [r| |/(_ O Logic.I)] // /(_ `|ceil r|%N Logic.I); rewrite /= in_itv /=.
+move=> [r| |/(_ O Logic.I)] // /(_ `|(ceil r)%real|%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.
@@ -2209,7 +2209,7 @@ have {}EBr2 : \esum_(i in E) mu (closure (B i)) <=
   by apply: bigcup_measurable => *; exact: measurable_closure.
 have finite_set_F i : finite_set (F i).
   apply: contrapT.
-  pose M := `|ceil ((r%:num + 2) *+ 2 / (1 / (2 ^ i.+1)%:R))|.+1.
+  pose M := `|(ceil ((r%:num + 2) *+ 2 / (1 / (2 ^ i.+1)%:R)))%real|.+1.
   move/(infinite_set_fset M) => [/= C] CsubFi McardC.
   have MC : (M%:R * (1 / (2 ^ i.+1)%:R))%:E <=
             mu (\bigcup_(j in [set` C]) closure (B j)).

theories/measure.v

@@ -2198,8 +2198,8 @@ Lemma infinite_card_dirac (A : set T) : infinite_set A ->
   \esum_(i in A) \d_ i A = +oo :> \bar R.
 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).
+have [B BA Br] := infinite_set_fset `|(ceil r)%real| infA.
+apply: esum_ge; exists [set` B] => //; apply: (@le_trans _ _ `|(ceil r)%real|%:R%:E).
   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.

theories/normedtype.v

@@ -252,10 +252,10 @@ End pseudoMetricnormedzmodule_lemmas.
 Lemma bigcup_ballT {R : realType} : \bigcup_n ball (0%R : R) n%:R = setT.
 Proof.
 apply/seteqP; split => // x _; have [x0|x0] := ltP 0%R x.
-  exists `|reals.ceil x|.+1 => //.
+  exists `|(ceil x)%real|.+1 => //.
   rewrite /ball /= sub0r normrN gtr0_norm// (le_lt_trans (ceil_ge _))//.
   by rewrite -natr1 natr_absz -abszE gtz0_abs// ?ceil_gt0// ltr_pwDr.
-exists `|reals.ceil (- x)|.+1 => //.
+exists `|(ceil (- x))%real|.+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.
@@ -596,7 +596,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 (le_trans (@ceil_ge R A))// (ler_int _ _ (f n)) [reals.ceil _]intEsign.
+rewrite (le_trans (@ceil_ge R A))// (ler_int _ _ (f n)) [(ceil _)%real]intEsign.
 by rewrite le_gtF ?expr0 ?mul1r ?lez_nat ?ceil_ge0//; near: n; apply: Foo.
 Unshelve. all: by end_near. Qed.
 
@@ -5779,7 +5779,7 @@ rewrite ler_pdivlMr// mulrC -ler_pdivlMr//.
 have [f0|f0] := eqVneq 0 f.
   by move: mf; rewrite -f0 absz0 leNgt expnS ltr_nat leq_pmulr// expn_gt0.
 rewrite (le_trans mf)// prednK//; last by rewrite absz_gt0 eq_sym.
-by rewrite natr_absz// ger0_norm// reals.floor_le.
+by rewrite natr_absz// ger0_norm// ge_floor// num_real.
 Qed.
 
 Lemma cover_vitali_collection_partition :

theories/real_interval.v

@@ -377,12 +377,12 @@ Proof.
 apply/seteqP; split => [x/=|]; last first.
   move=> x [n _ /=] /[!in_itv] /andP[-> /le_lt_trans]; apply.
   by rewrite ltrBlDr ltrDl invr_gt0 ltr0n.
-rewrite in_itv/= => /andP[sx xs]; exists `|ceil ((s - x)^-1)|%N => //=.
+rewrite in_itv/= => /andP[sx xs]; exists `|(ceil (s - x)^-1)%real|%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 (@le_trans _ _ (ceil (s - x)^-1)%:~R)// ?lerDl// ceil_ge.
+  by rewrite (@le_trans _ _ (ceil (s - x)^-1)%real%:~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.
 Qed.
@@ -404,7 +404,7 @@ Lemma itv_bnd_infty_bigcup (R : realType) b (x : R) :
 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.
+move=> xy; exists `|ceil (y - x)|%real%N => //=; rewrite in_itv/= xy/= -lerBlDl.
 rewrite !natr_absz/= ger0_norm ?ceil_ge0 ?subr_ge0 ?ceil_ge//.
 by case: b xy => //= /ltW.
 Qed.

theories/realfun.v

@@ -183,7 +183,7 @@ exists (fun n => sval (cid (He (PosNum (invn n))))).
   apply/cvgrPdist_lt => r r0; near=> t.
   rewrite /sval/=; case: cid => x [px xpt _].
   rewrite distrC (lt_le_trans xpt)// -(@invrK _ r) lef_pV2 ?posrE ?invr_gt0//.
-  near: t; exists `|ceil (r^-1)|%N => // s /=.
+  near: t; exists `|ceil (r^-1)|%real%N => // s /=.
   rewrite -ltnS -(@ltr_nat R) => /ltW; apply: le_trans.
   by rewrite natr_absz gtr0_norm ?ceil_gt0 ?invr_gt0// ceil_ge.
 move=> /cvgrPdist_lt/(_ e%:num (ltac:(by [])))[] n _ /(_ _ (leqnn _)).
@@ -233,8 +233,8 @@ have y_p : y_ n @[n --> \oo] --> p.
   rewrite ltrBlDr => /lt_le_trans; apply.
   rewrite addrC lerD2r -(invrK e) lef_pV2// ?posrE ?invr_gt0//.
   near: t.
-  exists `|ceil e^-1|%N => // k /= ek.
-  rewrite (le_trans (ceil_ge _))// (@le_trans _ _ `|ceil e^-1|%:~R)//.
+  exists `|ceil e^-1|%real%N => // k /= ek.
+  rewrite (le_trans (ceil_ge _))// (@le_trans _ _ `|ceil e^-1|%real%:~R)//.
     by rewrite ger0_norm// ?ceil_ge0// ?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).

theories/reals.v

@@ -240,6 +240,10 @@ End ToInt.
 (* -------------------------------------------------------------------- *)
 Reserved Notation "'floor' r" (at level 10).
 Notation "'floor' x" := (Num.floor x) : real_scope.
+
+Reserved Notation "'ceil' r" (at level 10).
+Notation "'ceil' x" := (Num.ceil x) : real_scope.
+
 Local Open Scope real_scope.
 
 Section RealDerivedOps.
@@ -248,14 +252,10 @@ Variable R : realType.
 Implicit Types x y : R.
 Definition floor_set x := [set y : R | (y \is a Rint) && (y <= x)].
 
-(*Definition floor x : int := Num.floor x.*)
-
 Definition Rfloor x : R := (floor x)%:~R.
 
 Definition range1 (x : R) := [set y | x <= y < x + 1].
 
-Definition ceil x := Num.ceil x.
-
 Definition Rceil x : R := (ceil x)%:~R.
 
 End RealDerivedOps.
@@ -491,8 +491,8 @@ Proof. by rewrite /Rfloor; exact: mem_rg1_floor. Qed.
 Lemma Rfloor_le x : Rfloor x <= x.
 Proof. by case/andP: (mem_rg1_Rfloor x). Qed.
 
-Lemma floor_le x : (floor x)%:~R <= x.
-Proof. by rewrite ge_floor// num_real. Qed.
+Lemma __deprecated__floor_le x : (floor x)%:~R <= x.
+Proof. by rewrite ge_floor ?num_real. Qed.
 
 Lemma lt_succ_Rfloor x : x < Rfloor x + 1.
 Proof. by case/andP: (mem_rg1_Rfloor x). Qed.
@@ -575,7 +575,7 @@ Lemma floor_neq0 x : (floor x != 0) = (x < 0) || (x >= 1).
 Proof.
 apply/idP/orP => [|[x0|/le_floor r1]]; first rewrite neq_lt => /orP[x0|x0].
 - by left; apply: contra_lt x0; rewrite floor_ge0.
-- by right; rewrite (le_trans _ (floor_le _))// ler1z -gtz0_ge1.
+- by right; rewrite (le_trans _ (ge_floor _)) ?num_real// ler1z -gtz0_ge1.
 - by rewrite lt_eqF//; apply: contra_lt x0; rewrite floor_ge0.
 - by rewrite gt_eqF// (lt_le_trans _ r1)// floor1.
 Qed.
@@ -610,13 +610,13 @@ Lemma isint_Rceil x : Rceil x \is a Rint.
 Proof. by rewrite /Rceil RintC. Qed.
 
 Lemma Rceil0 : Rceil 0 = 0 :> R.
-Proof. by rewrite /Rceil /ceil ceil0. Qed.
+Proof. by rewrite /Rceil ceil0. Qed.
 
 Lemma Rceil_ge x : x <= Rceil x.
 Proof. by rewrite /Rceil le_ceil// num_real. Qed.
 
 Lemma le_Rceil : {homo (@Rceil R) : x y / x <= y}.
-Proof. by move=> x y ?; rewrite /Rceil /ceil ler_int ceil_le. Qed.
+Proof. by move=> x y ?; rewrite /Rceil ler_int ceil_le. Qed.
 
 Lemma Rceil_ge0 x : 0 <= x -> 0 <= Rceil x.
 Proof. by move=> x0; rewrite /Rceil ler0z -(ceil0 R) ceil_le. Qed.
@@ -631,30 +631,30 @@ Lemma ceil_ge0 x : 0 <= x -> 0 <= ceil x.
 Proof. by move/(ge_trans (ceil_ge x)); rewrite -(ler_int R). Qed.
 
 Lemma ceil_gt0 x : 0 < x -> 0 < ceil x.
-Proof. by move=> ?; rewrite /ceil oppr_gt0 floor_lt0 // ltrNl oppr0. Qed.
+Proof. by move=> ?; rewrite oppr_gt0 floor_lt0 // ltrNl oppr0. Qed.
 
 Lemma ceil_le0 x : x <= 0 -> ceil x <= 0.
 Proof. by move=> x0; rewrite -lerNl oppr0 floor_ge0 -lerNr oppr0. Qed.
 
-Lemma le_ceil : {homo @ceil R : x y / x <= y}.
+Lemma le_ceil : {homo @Num.ceil R : x y / x <= y}.
 Proof. by move=> x y xy; rewrite lerNl opprK le_floor // lerNl opprK. Qed.
 
 Lemma ceil_ge_int x (z : int) : (x <= z%:~R) = (ceil x <= z).
-Proof. by rewrite /ceil; apply: ceil_le_int; rewrite num_real. Qed.
+Proof. by apply: ceil_le_int; rewrite num_real. Qed.
 
 Lemma ceil_lt_int x (z : int) : (z%:~R < x) = (z < ceil x).
 Proof. by rewrite ltNge ceil_ge_int -ltNge. Qed.
 
 Lemma ceilN x : ceil (- x) = - floor x. Proof.
-Proof. by rewrite /ceil /Num.ceil opprK. Qed.
+Proof. by rewrite /Num.ceil opprK. Qed.
 
-Lemma floorN x : floor (- x) = - ceil x. Proof. by rewrite /ceil opprK. Qed.
+Lemma floorN x : floor (- x) = - ceil x. Proof. by rewrite opprK. Qed.
 
 Lemma abs_ceil_ge x : `|x| <= `|ceil x|.+1%:R.
 Proof.
 rewrite -natr1 natr_absz; have [x0|x0] := ltP 0%R x.
   by rewrite !gtr0_norm ?ceil_gt0// (le_trans (ceil_ge _))// lerDl.
-rewrite !ler0_norm ?ceil_le0// /ceil opprK.
+rewrite !ler0_norm ?ceil_le0// opprK.
 by rewrite intr1; apply/ltW/lt_succ_floor; rewrite num_real.
 Qed.