From f6d2a6e2581ad7b8132e2f1123992c3551684490 Mon Sep 17 00:00:00 2001
From: Kazuhiko Sakaguchi <pi8027@gmail.com>
Date: Mon, 15 Jul 2024 18:21:28 +0200
Subject: [PATCH] Tidy some proofs

---
 classical/mathcomp_extra.v   | 11 +++--------
 theories/altreals/realsum.v  | 14 ++++++--------
 theories/lebesgue_integral.v |  2 +-
 theories/lebesgue_measure.v  |  4 ++--
 4 files changed, 12 insertions(+), 19 deletions(-)

diff --git a/classical/mathcomp_extra.v b/classical/mathcomp_extra.v
index 774c2194b4..fa364a20d7 100644
--- a/classical/mathcomp_extra.v
+++ b/classical/mathcomp_extra.v
@@ -399,20 +399,15 @@ Proof. by rewrite ltNge floor_ge_int -ltNge. Qed.
 Lemma floor_ge0 x : (0 <= Num.floor x) = (0 <= x).
 Proof. by rewrite -floor_ge_int. Qed.
 
-Lemma floor_le0 x : x < 1 -> Num.floor x <= 0.
-Proof.
-by rewrite (_ : 1 = 1%:~R)// floor_lt_int -ltzD1 add0r => /le_lt_trans; exact.
-Qed.
+Lemma floor_le0 x : (x < 1) = (Num.floor x <= 0).
+Proof. by rewrite -ltzD1 add0r -floor_lt_int. Qed.
 
-Lemma floor_lt0 x : x < 0 -> Num.floor x < 0.
+Lemma floor_lt0 x : (x < 0) = (Num.floor x < 0).
 Proof. by rewrite -floor_lt_int. Qed.
 
 Lemma lt_succ_floor x : x < (Num.floor x + 1)%:~R.
 Proof. exact: Num.Theory.lt_succ_floor. Qed.
 
-Lemma floor_natz n : Num.floor (n%:R : R) = n%:~R :> int.
-Proof. by rewrite (Num.Theory.intrKfloor n) intz. Qed.
-
 Lemma floor_neq0 x : (Num.floor x != 0) = (x < 0) || (x >= 1).
 Proof. by rewrite neq_lt -floor_lt_int gtz0_ge1 -floor_ge_int. Qed.
 
diff --git a/theories/altreals/realsum.v b/theories/altreals/realsum.v
index cc88039f48..900f467cea 100644
--- a/theories/altreals/realsum.v
+++ b/theories/altreals/realsum.v
@@ -141,16 +141,14 @@ Lemma summable_countn0 : summable f -> countable [pred x | f x != 0].
 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 := `|Num.floor (`|f x|^-1)|%N; exists j; rewrite inE.
-  rewrite mul1r invf_plt ?unfold_in /= ?ltr0z ?normr_gt0 // /j -addn1 /=.
-  by rewrite PoszD gez0_abs ?floor_ge0 ?invr_ge0 ?normr_ge0// lt_succ_floor.
+  move=> x; rewrite !inE => nz_fx; exists (Num.trunc `|f x|^-1).
+  rewrite inE mul1r invf_plt ?unfold_in /= ?normr_gt0 //.
+  by have/trunc_itv/andP[]: 0 <= `|f x|^-1 by rewrite invr_ge0 normr_ge0.
 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 := `|Num.floor (M / i.+1%:R)|.+1.
-pose K := (`|Num.floor M|.+1 * i.+1)%N; move/(_ K)/asboolP/exists_asboolP.
-move=> h; have /asboolP[] := xchooseP h.
+move=> /finiteNP/(_ ((Num.trunc M).+1 * i.+1)%N)/asboolP/exists_asboolP 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.
 apply/(@lt_le_trans _ _ (\sum_(x : J) 1 / i.+1%:~R)); last first.
@@ -158,7 +156,7 @@ apply/(@lt_le_trans _ _ (\sum_(x : J) 1 / i.+1%:~R)); last first.
   by have:= fsvalP m; rewrite in_fset => /le_sEi.
 rewrite mul1r sumr_const -cardfE card_fseq undup_id // eq_si.
 rewrite -mulr_natr natrM mulrC mulfK ?pnatr_eq0//.
-by rewrite pmulrn -addn1 PoszD gez0_abs ?floor_ge0// lt_succ_floor.
+by case/trunc_itv/andP: ge0_M.
 Qed.
 
 End SummableCountable.
diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v
index 7683f2728f..e0a91dd302 100644
--- a/theories/lebesgue_integral.v
+++ b/theories/lebesgue_integral.v
@@ -1586,7 +1586,7 @@ case/cvg_ex => /= l; have [l0|l0] := leP 0%R l.
   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).
+  by rewrite -(@lez0_abs (floor _))// -floor_le0// (lt_le_trans l0).
 Qed.
 
 Lemma ecvg_approx (f0 : forall x, D x -> (0 <= f x)%E) x :
diff --git a/theories/lebesgue_measure.v b/theories/lebesgue_measure.v
index 4d184c1bc4..8e2741f298 100644
--- a/theories/lebesgue_measure.v
+++ b/theories/lebesgue_measure.v
@@ -1159,7 +1159,7 @@ rewrite predeqE => t; split => [/= [Dt ft]|].
       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.
-    rewrite natr_absz ltr0_norm ?floor_lt0// EFinN.
+    rewrite natr_absz ltr0_norm -?floor_lt0// EFinN.
     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.
@@ -1407,7 +1407,7 @@ move=> /(_ `|floor r|%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.
-  by rewrite ltrNr oppr0 floor_lt0.
+  by rewrite ltrNr oppr0 -floor_lt0.
 by rewrite mulrNz lerNl opprK ge_floor.
 Qed.