Remove abs_ceil_ge (#1818)

Author: pi8027

classical/unstable.v

@@ -409,20 +409,6 @@ Proof. by rewrite intrD. Qed.
 Lemma intr1D {R : pzRingType} (i : int) : 1 + i%:~R = (1 + i)%:~R :> R.
 Proof. by rewrite intrD. Qed.
 
-Section trunc_floor_ceil.
-Context {R : archiRealDomainType}.
-Implicit Type x : R.
-
-(* PR in progress: https://github.com/math-comp/math-comp/pull/1515 *)
-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.ceil_ge _))// lerDl.
-by rewrite !ler0_norm ?ceil_le0// ?ceilNfloor opprK intrD1 ltW// floorD1_gt.
-Qed.
-
-End trunc_floor_ceil.
-
 Section bijection_forall.
 
 Lemma bij_forall A B (f : A -> B) (P : B -> Prop) :

theories/lebesgue_integral_theory/lebesgue_integral_differentiation.v

@@ -1076,21 +1076,21 @@ have fE y k r : (ball 0%R k.+1%:R) y -> (r < 1)%R ->
   rewrite (lt_le_trans xrt)// lerBlDl (le_trans (ltW r1))//.
   rewrite -lerBlDl addrC -lerBrDr (le_trans (ler_norm _))// normrN.
   by rewrite (le_trans (ltW yk1))// lerBrDr natr1 ler_nat -muln2 ltn_Pmulr.
-have := h `|ceil x|.+1%N Logic.I.
-have Bxx : B `|ceil x|.+1 x.
-  rewrite /B /ball/= sub0r normrN (le_lt_trans (unstable.abs_ceil_ge _))// ltr_nat.
-  by rewrite -addnn addSnnS ltn_addl.
+have := h (truncn `|x|) Logic.I.
+have Bxx : B (truncn `|x|) x.
+  rewrite /B /ball/= sub0r normrN doubleS -truncn_le_nat.
+  by rewrite -addnn -addnS leq_addr.
 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 `|ceil x|.+1 y - fk `|ceil x|.+1 x|%:E.
+  \int[mu]_(y in ball x t) `|fk (truncn `|x|) y - fk (truncn `|x|) x|%:E.
   near=> t.
   apply: eq_integral => /= y /[1!inE] xty.
   rewrite -(fE x _ t)//; last first.
-    by rewrite /ball/= sub0r normrN (le_lt_trans (unstable.abs_ceil_ge _))// ltr_nat.
+    by rewrite /ball/= sub0r normrN -truncn_le_nat.
   rewrite -(fE x _ t)//; last first.
     by apply: ballxx; near: t; exact: nbhs_right_gt.
-  by rewrite /ball/= sub0r normrN (le_lt_trans (unstable.abs_ceil_ge _))// ltr_nat.
+  by rewrite /ball/= sub0r normrN -truncn_le_nat.
 apply/fine_cvgP; split=> [{davg_fk0}|{davg_fk_fin_num}].
 - move: davg_fk_fin_num => -[M /= M0] davg_fk_fin_num.
   apply: filter_app f_fk_ceil; near=> t => Ht.

theories/normedtype_theory/num_normedtype.v

@@ -560,9 +560,9 @@ move=> dF nyF; rewrite itvNy_bnd_bigcup_BLeft eqEsubset; split.
     by exists (truncn (z - a)); rewrite zFan// -ltrBlDl truncnS_gt.
   by exists i => //=; rewrite in_itv/= yFa (lt_le_trans _ Fany).
 - move=> z/= [n _ /=]; rewrite in_itv/= => /andP[Fanz zFa].
-  exists `|ceil (F (a + n.+1%:R) - F a)%R|.+1 => //=.
-  rewrite in_itv/= zFa andbT lerBlDr -lerBlDl (le_trans _ (abs_ceil_ge _))//.
-  by rewrite ler_normr orbC opprB lerB// ltW.
+  exists (truncn (F a - F (a + n.+1%:R))).+1 => //=.
+  rewrite in_itv/= zFa andbT lerBlDr -lerBlDl ltW//.
+  by rewrite -truncn_le_nat le_truncn// lerB// ltW.
 Qed.
 
 Lemma decreasing_itvoo_bigcup F a n :
@@ -586,14 +586,13 @@ move=> dF nyF; rewrite itvNy_bnd_bigcup_BLeft eqEsubset; split.
 - move=> y/= [n _]/=; rewrite in_itv/= => /andP[Fany yFa].
   have [i iFan] : exists i, F (a - i.+1%:R) < F a - n%:R.
     move/cvgrNy_lt : nyF => /(_ (F a - n%:R))[z [zreal zFan]].
-    exists `|ceil (a - z)|%N.
-    rewrite zFan// ltrBlDr -ltrBlDl (le_lt_trans (ceil_ge _)) ?num_real//.
-    by rewrite (le_lt_trans (ler_norm _))// -natr1 -intr_norm ltrDl.
+    exists (truncn (a - z)).
+    by rewrite zFan// ltrBlDr -ltrBlDl -truncn_le_nat.
   by exists i => //=; rewrite in_itv/= yFa andbT (lt_le_trans _ Fany).
 - move=> z/= [n _ /=]; rewrite in_itv/= => /andP[Fanz zFa].
-  exists `|ceil (F (a - n.+1%:R) - F a)|.+1 => //=.
-  rewrite in_itv/= zFa andbT lerBlDr -lerBlDl (le_trans _ (abs_ceil_ge _))//.
-  by rewrite ler_normr orbC opprB lerB// ltW.
+  exists (truncn (F a - F (a - n.+1%:R))).+1 => //=.
+  rewrite in_itv/= zFa andbT lerBlDr -lerBlDl ltW//.
+  by rewrite -truncn_le_nat le_truncn// lerB// ltW.
 Qed.
 
 Lemma increasing_itvoc_bigcup F a n :