Fix deprecation warnings about ceil_ge

reals/real_interval.v

@@ -275,7 +275,7 @@ 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 (lt_le_trans (ltrN10 R))// 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)%:~R)// ?lerDl// le_ceil/=.
 - 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.
@@ -298,9 +298,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 ?ceil_ge//.
-rewrite (lt_le_trans (ltrN10 R))// subr_ge0.
-by case: b xy => //= /ltW.
+rewrite natr_absz ger0_norm ?le_ceil//=.
+by rewrite -ceil_ge0 (lt_le_trans (ltrN10 R))// subr_ge0 (lteifW xy).
 Qed.
 
 Lemma itv_infty_bnd_bigcup (R : realType) b (x : R) :
@@ -310,7 +309,7 @@ Proof.
 have /(congr1 (fun x => -%R @` x)) := itv_bnd_infty_bigcup (~~ b) (- x).
 rewrite opp_itv_bnd_infty negbK opprK => ->; rewrite image_bigcup.
 apply eq_bigcupr => k _; apply/seteqP; split=> [_ /= -[r rbxk <-]|y/= yxkb].
-   by rewrite oppr_itv/= opprB addrC.
+  by rewrite oppr_itv/= opprB addrC.
 by exists (- y); [rewrite oppr_itv/= negbK opprD opprK|rewrite opprK].
 Qed.
 

reals/reals.v

@@ -116,9 +116,9 @@ End has_bound_lemmas.
 (* -------------------------------------------------------------------- *)
 
 HB.mixin Record ArchimedeanField_isReal R of Num.ArchiField R := {
-  sup_upper_bound_subdef : forall E : set [the archiFieldType of R],
+  sup_upper_bound_subdef : forall E : set R,
     has_sup E -> ubound E (supremum 0 E) ;
-  sup_adherent_subdef : forall (E : set [the archiFieldType of R]) (eps : R),
+  sup_adherent_subdef : forall (E : set R) (eps : R),
     0 < eps -> has_sup E -> exists2 e : R, E e & (supremum 0 E - eps) < e
 }.
 

theories/lebesgue_integral.v

@@ -1548,19 +1548,15 @@ 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=> /(_ (`|ceil l|.+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 (ceil _)) // -ceil_ge0 (lt_le_trans _ l0).
+  move=> /(_ (`|ceil l|.+1 + n)%N) /= /(_ (leq_addl _ _)); apply/negP.
+  rewrite -leNgt approx_x distrC (le_trans _ (lerB_normD _ _))// normrN.
+  rewrite lerBrDl addSnnS natrD [leRHS]ger0_norm// lerD ?ler1n// natr_absz.
+  by rewrite !ger0_norm ?le_ceil// -ceil_ge0; apply: 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 _ _))//.
-  rewrite normrN lerBrDl addSnnS [leRHS]ger0_norm ?ler0n//.
-  rewrite natrD lerD ?ler1n// ltr0_norm// (@le_trans _ _ (- floor l)%:~R)//.
-    by rewrite mulrNz lerNl opprK ge_floor.
-  by rewrite -(@lez0_abs (floor _))// -floor_le0// (lt_le_trans l0).
+  rewrite approx_x -leNgt distrC (le_trans _ (lerB_normD _ _))// normrN.
+  rewrite lerBrDl addSnnS natrD [leRHS]ger0_norm// lerD ?ler1n// natr_absz.
+  by rewrite !ltr0_norm -?floor_lt0// mulrNz lerN2 ge_floor.
 Qed.
 
 Lemma ecvg_approx (f0 : forall x, D x -> (0 <= f x)%E) x :
@@ -2330,22 +2326,20 @@ transitivity (\int[mu]_(x in D) limn (g^~ x)).
   - rewrite gt0_mulye//; apply/cvgeyPgey; near=> M.
     have M0 : (0 <= M)%R by [].
     rewrite /g; case: (f x) fx0 => [r r0|_|//]; last first.
-      exists 1%N => // m /= m0.
-      by rewrite mulry gtr0_sg// ?mul1e ?leey// ltr0n.
+      by exists 1%N => // m /= m0; rewrite mulry gtr0_sg// ?ltr0n// mul1e leey.
     near=> n; rewrite lee_fin -ler_pdivrMr//.
     near: n; exists `|ceil (M / r)|%N => // m /=.
     rewrite -(ler_nat R); apply: le_trans.
-    rewrite natr_absz ger0_norm ?ceil_ge// -ceil_ge0// (lt_le_trans (ltrN10 _))//.
-    by rewrite divr_ge0// ?ltW.
+    rewrite natr_absz ger0_norm ?le_ceil//= -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.
-      exists 1%N => // m /= m0.
-      by rewrite mulrNy gtr0_sg// ?ltr0n// mul1e ?leNye.
+      by exists 1%N => // m /= m0; rewrite mulrNy gtr0_sg// ?ltr0n// mul1e leNye.
     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// (lt_le_trans (ltrN10 _))//.
+    rewrite natr_absz ger0_norm ?le_ceil//= -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*)
@@ -2367,7 +2361,7 @@ 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 ?le_ceil//= -ceil_ge0//.
 rewrite (lt_le_trans (ltrN10 _))//.
 by rewrite mulr_ge0// ?invr_ge0//; exact/fine_ge0/integral_ge0.
 Unshelve. all: by end_near. Qed.
@@ -2607,7 +2601,7 @@ have <- : (fun t => limn (g^~ t)) = cst +oo.
   rewrite funeqE => t; apply/cvg_lim => //=.
   apply/cvgeryP/cvgryPge => M; exists `|ceil M|%N => //= m.
   rewrite /= -(ler_nat R); apply: le_trans.
-  by rewrite (le_trans (ceil_ge _))// natr_absz ler_int ler_norm.
+  by rewrite (le_trans (le_ceil _))//= natr_absz ler_int ler_norm.
 rewrite monotone_convergence //.
 - under [in LHS]eq_fun do rewrite integral_cstr.
   apply/cvg_lim => //; apply/cvgeyPge => M.
@@ -2618,7 +2612,7 @@ rewrite monotone_convergence //.
   rewrite -(ler_nat R) => MDm; rewrite -(@fineK _ (mu D)) ?ge0_fin_numE//.
   rewrite -lee_pdivrMr; last by rewrite fine_gt0// lt0e muD0 measure_ge0.
   rewrite lee_fin (le_trans _ MDm)//.
-  by rewrite natr_absz (le_trans (ceil_ge _))// ler_int ler_norm.
+  by rewrite natr_absz (le_trans (le_ceil _))//= ler_int ler_norm.
 - by move=> n; exact: measurable_cst.
 - by move=> n x Dx; rewrite lee_fin.
 - by move=> t Dt n m nm; rewrite /g lee_fin ler_nat.
@@ -3479,7 +3473,7 @@ rewrite -[X in _ * X](@fineK _ (mu (E `&` D))); last first.
   by rewrite fin_numElt muEDoo (lt_le_trans _ (measure_ge0 _ _)).
 rewrite lte_fin -ltr_pdivrMr.
   rewrite -natr1 natr_absz ger0_norm.
-    by rewrite (le_lt_trans (ceil_ge _))// ltrDl.
+    by rewrite (le_lt_trans (le_ceil _))//= ltrDl.
   by rewrite -ceil_ge0// (lt_le_trans (ltrN10 _))// divr_ge0.
 rewrite -lte_fin fineK.
   rewrite lt0e measure_ge0 andbT.
@@ -3745,7 +3739,7 @@ move=> mf; split=> [iDf0|Df0].
       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 rewrite lerD2r// le_ceil.
     by split => //; apply: contraTN nft => /eqP ->; rewrite abse0 -ltNge.
   transitivity (limn (fun n => mu (D `&` [set x | `|f x| >= n.+1%:R^-1%:E]))).
     apply/esym/cvg_lim => //; apply: nondecreasing_cvg_mu.

theories/lebesgue_measure.v

@@ -458,7 +458,7 @@ rewrite predeqE => t; split => [/= [Dt ft]|].
       by rewrite -{2}(fineK ft)// lee_fin (le_trans _ ft0)// lerNl oppr0.
     rewrite natr_absz ger0_norm; last first.
       by rewrite -ceil_ge0 (lt_le_trans _ ft0).
-    by rewrite -(fineK ft) lee_fin ceil_ge.
+    by rewrite -(fineK ft) lee_fin le_ceil/=.
   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.
@@ -718,7 +718,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// ?le_ceil// -ceil_gt0.
 Qed.
 
 End erealwithrays.
@@ -2856,7 +2856,7 @@ have finite_set_F i : finite_set (F i).
   apply/negP; rewrite -ltNge lebesgue_measure_ball// lte_fin.
   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.
+  by rewrite -ltr_pdivrMr// -ltrBlDr (lt_le_trans _ (le_ceil _))// 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)) =
@@ -3188,7 +3188,7 @@ have bigBG_fin (r : {posnum R}) : finite_set (bigB G r%:num).
           by rewrite lee_fin ler_wpM2l// ler_nat count_predT.
         rewrite EFinM -lte_pdivrMl// muleC -(@fineK _ (mu O)); last first.
           by rewrite ge0_fin_numE//; case/andP: OAoo => ?; exact: lt_trans.
-        rewrite -EFinM /M lte_fin (le_lt_trans (ceil_ge _))//.
+        rewrite -EFinM /M lte_fin (le_lt_trans (le_ceil _))//=.
         rewrite -natr1 natr_absz ger0_norm ?ltrDl//.
         by rewrite -ceil_ge0// (@lt_le_trans _ _ 0%R)// divr_ge0// fine_ge0.
       rewrite big_seq [in leRHS]big_seq.

theories/measure.v

@@ -2308,7 +2308,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// le_ceil/=.
 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

@@ -276,10 +276,10 @@ 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 `|ceil x|.+1 => //.
-  rewrite /ball /= sub0r normrN gtr0_norm// (le_lt_trans (ceil_ge _))//.
+  rewrite /ball /= sub0r normrN gtr0_norm// (le_lt_trans (le_ceil _))//=.
   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 /ball /= sub0r normrN ler0_norm// (le_lt_trans (le_ceil _))//=.
 rewrite -natr1 natr_absz -abszE gez0_abs ?ltr_pwDr// -ceil_ge0 ltrNl opprK.
 by rewrite (le_lt_trans x0).
 Qed.
@@ -643,7 +643,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)) [ceil _]intEsign.
+rewrite (le_trans (le_ceil _)) // pmulrn ler_int [ceil _]intEsign.
 by rewrite le_gtF ?expr0 ?mul1r ?lez_nat -?ceil_ge0//; near: n; apply: Foo.
 Unshelve. all: by end_near. Qed.
 

theories/realfun.v

@@ -187,7 +187,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// le_ceil/=.
 move=> /cvgrPdist_lt/(_ e%:num (ltac:(by [])))[] n _ /(_ _ (leqnn _)).
 rewrite /sval/=; case: cid => // x [px xpn].
 by rewrite leNgt distrC => /negP.
@@ -250,7 +250,7 @@ have y_p : y_ n @[n --> \oo] --> p.
   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)//.
+  rewrite (le_trans (le_ceil _))//= (@le_trans _ _ `|ceil e^-1|%:~R)//.
     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).

theories/sequences.v

@@ -2978,7 +2978,7 @@ have : cvg (a @ \oo).
       exists `|ceil eps^-1|%N.
       rewrite -ltf_pV2 ?(posrE,divr_gt0)// invrK -addn1 natrD.
       rewrite natr_absz gtr0_norm.
-        by rewrite (le_lt_trans (ceil_ge _)) // ltrDl.
+        by rewrite (le_lt_trans (le_ceil _)) //= ltrDl.
       by rewrite -ceil_gt0 invr_gt0 divr_gt0.
     exists n.+1; rewrite -ltr_pdivlMl //.
     have /lt_trans : (r n.+1)%:num < n.+1%:R^-1.
@@ -3081,7 +3081,7 @@ have O_infempty : O_inf = set0.
   rewrite -subset0 => x.
   have [M FxM] := BoundedF x; rewrite /O_inf /O /=.
   move=> /(_ `|ceil M|%N Logic.I)[f Ff]; apply/negP; rewrite -leNgt.
-  rewrite (le_trans (FxM _ Ff))// (le_trans (ceil_ge _))//.
+  rewrite (le_trans (FxM _ Ff))// (le_trans (le_ceil _))//=.
   by have := lez_abs (ceil M); rewrite -(@ler_int K).
 have ContraBaire : exists i, not (dense (O i)).
   have dOinf : ~ dense O_inf.

theories/topology_theory/nat_topology.v

@@ -42,7 +42,7 @@ Lemma nbhs_infty_ger {R : realType} (r : R) :
   \forall n \near \oo, (r <= n%:R)%R.
 Proof.
 exists `|Num.ceil r|%N => // n /=; rewrite -(ler_nat R); apply: le_trans.
-by rewrite (le_trans (ceil_ge _))// natr_absz ler_int ler_norm.
+by rewrite (le_trans (le_ceil _))//= natr_absz ler_int ler_norm.
 Qed.
 
 Lemma cvg_addnl N : addn N @ \oo --> \oo.