From fcd8e8b9326f7cf9ecc41dcde4c1bd90551060b1 Mon Sep 17 00:00:00 2001
From: Kazuhiko Sakaguchi <pi8027@gmail.com>
Date: Fri, 29 Nov 2024 16:21:55 +0100
Subject: [PATCH] replace some `|Num.floor _| with Num.trunc _

---
 classical/mathcomp_extra.v |  3 +++
 reals/real_interval.v      | 20 ++++++--------------
 reals/reals.v              |  8 ++------
 3 files changed, 11 insertions(+), 20 deletions(-)

diff --git a/classical/mathcomp_extra.v b/classical/mathcomp_extra.v
index f7c05dd23..71fdf34c6 100644
--- a/classical/mathcomp_extra.v
+++ b/classical/mathcomp_extra.v
@@ -433,6 +433,9 @@ Section floor_ceil.
 Context {R : archiDomainType}.
 Implicit Type x : R.
 
+Lemma lt_succ_trunc x : x < (Num.trunc x).+1%:R.
+Proof. by have [/Num.Theory.trunc_itv/andP[]//|/lt_le_trans->] := leP 0 x. Qed.
+
 Lemma ge_floor x : (Num.floor x)%:~R <= x.
 Proof. exact: Num.Theory.ge_floor. Qed.
 
diff --git a/reals/real_interval.v b/reals/real_interval.v
index 15db5ad76..934140717 100644
--- a/reals/real_interval.v
+++ b/reals/real_interval.v
@@ -150,10 +150,8 @@ 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 /= 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// intrD1 lt_succ_floor.
+rewrite in_itv /= andbT => xy; exists (trunc y).+1 => //=.
+by rewrite in_itv /= xy /= lt_succ_trunc.
 Qed.
 
 Lemma itv_o_inftyEbigcup x :
@@ -240,12 +238,8 @@ 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|%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 intrD1 ltW// lt_succ_floor.
-- by rewrite posrE// ltr_pwDr// ler0z floor_ge0 invr_ge0 ltW.
-- by rewrite posrE invr_gt0.
+rewrite lte_fin -subr_gt0 => fgx; exists (trunc (fx - gx)^-1) => //.
+by rewrite /E/= fxE gxE lee_fin invf_ple ?posrE//; apply/ltW/lt_succ_trunc.
 Qed.
 
 End set_ereal.
@@ -257,10 +251,8 @@ 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|%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 intrD1 lt_succ_floor.
+have := rx (trunc e^-1) I; rewrite /= in_itv => /andP[/le_lt_trans->]//.
+by rewrite lerB// invf_ple ?posrE//; apply/ltW/lt_succ_trunc.
 Qed.
 
 Lemma itv_bnd_open_bigcup (R : realType) b (r s : R) :
diff --git a/reals/reals.v b/reals/reals.v
index 2b1fd3ad1..c6a76c5d1 100644
--- a/reals/reals.v
+++ b/reals/reals.v
@@ -529,12 +529,8 @@ Proof. exact: Num.Theory.floor_le. Qed.
 
 Lemma ltr_add_invr (y x : R) : y < x -> exists k, y + k.+1%:R^-1 < x.
 Proof.
-move=> yx; exists `|floor (x - y)^-1|%N.
-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 intrD1 lt_succ_floor.
+move=> yx; exists (trunc (x - y)^-1).
+by rewrite -ltrBrDl invf_plt 1?posrE 1?subr_gt0// lt_succ_trunc.
 Qed.
 
 End FloorTheory.