Tidy some proofs

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.
 

theories/altreals/realsum.v

@@ -141,24 +141,22 @@ 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.
   apply/ler_sum=> /= m _; apply/ltW.
   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.

theories/lebesgue_integral.v

@@ -1287,22 +1287,20 @@ Qed.
 Lemma bigsetU_dyadic_itv n : `[n%:R, n.+1%:R[%classic =
   \big[setU/set0]_(n * 2 ^ n.+1 <= k < n.+1 * 2 ^ n.+1) [set` I n.+1 k].
 Proof.
-rewrite predeqE => r; split => [/= /[!in_itv]/= /andP[nr rn1]|].
-- rewrite -bigcup_seq /=; exists `|floor (r * 2 ^+ n.+1)|%N.
-    rewrite /= mem_index_iota -ltz_nat -lez_nat gez0_abs ?floor_ge0; last first.
-      by rewrite mulr_ge0// (le_trans _ nr).
-    rewrite -floor_ge_int -floor_lt_int.
-    by rewrite !PoszM -!natrXE !rmorphM !rmorphXn /= ler_wpM2r ?ltr_pM2r.
-  rewrite /= in_itv /=; apply/andP; split.
-    rewrite ler_pdivrMr// (le_trans _ (ge_floor _)) //.
-    by rewrite -(@gez0_abs (floor _))// floor_ge0 mulr_ge0// (le_trans _ nr).
-  rewrite ltr_pdivlMr// (lt_le_trans (lt_succ_floor _))//.
-  rewrite -[in leRHS]natr1 -intr1 lerD2r// -(@gez0_abs (floor _))// floor_ge0.
-  by rewrite mulr_ge0// (le_trans _ nr).
-- rewrite -bigcup_seq => -[/= k] /[!mem_index_iota] /andP[nk kn].
-  rewrite in_itv /= => /andP[knr rkn]; rewrite in_itv /=; apply/andP; split.
+rewrite predeqE => r; split => [/= /[!in_itv]/= /andP[nr rn1]|]; last first.
+  rewrite -bigcup_seq => -[/= k] /[!mem_index_iota] /andP[nk kn].
+  rewrite !in_itv /= => /andP[knr rkn]; apply/andP; split.
     by rewrite (le_trans _ knr)// ler_pdivlMr// -natrX -natrM ler_nat.
   by rewrite (lt_le_trans rkn)// ler_pdivrMr// -natrX -natrM ler_nat.
+rewrite -bigcup_seq /=; exists `|floor (r * 2 ^+ n.+1)|%N.
+  rewrite /= mem_index_iota -ltz_nat -lez_nat gez0_abs; last first.
+    by rewrite floor_ge0 mulr_ge0// (le_trans _ nr).
+  rewrite -floor_ge_int -floor_lt_int.
+  by rewrite !PoszM -!natrXE !rmorphM !rmorphXn /= ler_wpM2r ?ltr_pM2r.
+rewrite /= in_itv /= ler_pdivrMr// ltr_pdivlMr//.
+rewrite pmulrn [(`|_|.+1%:R)]pmulrn intS addrC gez0_abs; last first.
+  by rewrite floor_ge0 mulr_ge0 ?exprn_ge0 // (le_trans _ nr).
+by rewrite ge_floor lt_succ_floor.
 Qed.
 
 Lemma dyadic_itv_image n T (f : T -> \bar R) x :
@@ -1586,7 +1584,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 :

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.
 

theories/topology.v

@@ -2282,7 +2282,7 @@ Proof. by exists N. Qed.
 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.
+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.
 Qed.