Tidy some proofs

classical/mathcomp_extra.v

@@ -388,64 +388,56 @@ Context {R : archiDomainType}.
 Implicit Type x : R.
 
 Lemma ge_floor x : (Num.floor x)%:~R <= x.
-Proof. by rewrite Num.Theory.ge_floor. Qed.
+Proof. exact: Num.Theory.ge_floor. Qed.
+
+Lemma floor_ge_int x (z : int) : (z%:~R <= x) = (z <= Num.floor x).
+Proof. exact: Num.Theory.floor_ge_int. Qed.
+
+Lemma floor_lt_int x (z : int) : (x < z%:~R) = (Num.floor x < z).
+Proof. by rewrite ltNge floor_ge_int -ltNge. Qed.
 
 Lemma floor_ge0 x : (0 <= Num.floor x) = (0 <= x).
-Proof. by rewrite -Num.Theory.floor_ge_int. Qed.
+Proof. by rewrite -floor_ge_int. Qed.
 
 Lemma floor_le0 x : x <= 0 -> Num.floor x <= 0.
 Proof. by move/Num.Theory.floor_le; rewrite Num.Theory.floor0. Qed.
 
 Lemma floor_lt0 x : x < 0 -> Num.floor x < 0.
-Proof. by move=> x0; rewrite -(@ltrz0 R) (le_lt_trans (ge_floor _)). Qed.
+Proof. by rewrite -floor_lt_int. Qed.
 
 Lemma lt_succ_floor x : x < (Num.floor x + 1)%:~R.
-Proof. by rewrite Num.Theory.lt_succ_floor. Qed.
+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.floor_def _ _ n%:~R)// intr1 !mulrz_nat lexx/= ltr_nat addn1.
-Qed.
-
-Lemma floor_ge_int x (z : int) : (z%:~R <= x) = (z <= Num.floor x).
-Proof. by rewrite Num.Theory.floor_ge_int. Qed.
+Proof. by rewrite (Num.Theory.intrKfloor n) intz. Qed.
 
 Lemma floor_neq0 x : (Num.floor x != 0) = (x < 0) || (x >= 1).
-Proof.
-apply/idP/orP => [|[x0|/Num.Theory.floor_le r1]]; first rewrite neq_lt => /orP[x0|x0].
-- by left; apply: contra_lt x0; rewrite -floor_ge_int.
-- by right; rewrite (le_trans _ (ge_floor _))// ler1z -gtz0_ge1.
-- by rewrite lt_eqF//; apply: contra_lt x0; rewrite -floor_ge_int.
-- by rewrite gt_eqF// (lt_le_trans _ r1)// Num.Theory.floor1.
-Qed.
-
-Lemma floor_lt_int x (z : int) : (x < z%:~R) = (Num.floor x < z).
-Proof. by rewrite ltNge Num.Theory.floor_ge_int// -ltNge. Qed.
+Proof. by rewrite neq_lt -floor_lt_int gtz0_ge1 -floor_ge_int. Qed.
 
 Lemma ceil_ge x : x <= (Num.ceil x)%:~R.
-Proof. by rewrite Num.Theory.le_ceil. Qed.
+Proof. exact: Num.Theory.le_ceil. Qed.
+
+Lemma ceil_ge_int x (z : int) : (x <= z%:~R) = (Num.ceil x <= z).
+Proof. exact: Num.Theory.ceil_le_int. Qed.
+
+Lemma ceil_lt_int x (z : int) : (z%:~R < x) = (z < Num.ceil x).
+Proof. by rewrite ltNge ceil_ge_int -ltNge. Qed.
 
 Lemma ceil_ge0 x : 0 <= x -> 0 <= Num.ceil x.
 Proof. by move/(ge_trans (ceil_ge x)); rewrite -(ler_int R). Qed.
 
 Lemma ceil_gt0 x : 0 < x -> 0 < Num.ceil x.
-Proof. by move=> ?; rewrite oppr_gt0 floor_lt0 // ltrNl oppr0. Qed.
+Proof. by rewrite -ceil_lt_int. Qed.
 
 Lemma ceil_le0 x : x <= 0 -> Num.ceil x <= 0.
-Proof. by move=> x0; rewrite -lerNl oppr0 floor_ge0 -lerNr oppr0. Qed.
-
-Lemma ceil_ge_int x (z : int) : (x <= z%:~R) = (Num.ceil x <= z).
-Proof. by rewrite Num.Theory.ceil_le_int. Qed.
-
-Lemma ceil_lt_int x (z : int) : (z%:~R < x) = (z < Num.ceil x).
-Proof. by rewrite ltNge ceil_ge_int -ltNge. Qed.
+Proof. by rewrite -ceil_ge_int. Qed.
 
 Lemma ceilN x : Num.ceil (- x) = - Num.floor x.
 Proof. by rewrite /Num.ceil opprK. Qed.
 
 Lemma abs_ceil_ge x : `|x| <= `|Num.ceil x|.+1%:R.
 Proof.
-rewrite -natr1 natr_absz; have [x0|x0] := ltP 0%R x.
+rewrite -natr1 natr_absz; have [x0|x0] := ltP 0 x.
   by rewrite !gtr0_norm ?ceil_gt0// (le_trans (ceil_ge _))// lerDl.
 by rewrite !ler0_norm ?ceil_le0// opprK intr1 ltW// lt_succ_floor.
 Qed.

theories/altreals/realsum.v

@@ -141,11 +141,10 @@ 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 (1 / `|f x|)|%N; exists j; rewrite inE.
-  rewrite ltr_pdivrMr ?ltr0z // -ltr_pdivrMl ?normr_gt0 //.
-  rewrite mulr1 /j div1r -addn1 /= PoszD intrD mulr1z.
-  rewrite gez0_abs ?floor_ge0 ?invr_ge0 ?normr_ge0//.
-  by rewrite intr1 mathcomp_extra.lt_succ_floor.
+  pose j := `|Num.floor (`|f x|^-1)|%N; exists j; rewrite inE.
+  rewrite mul1r invf_plt ?unfold_in /= ?ltr0z ?normr_gt0 //.
+  rewrite /j -addn1 /= PoszD gez0_abs ?floor_ge0 ?invr_ge0 ?normr_ge0//.
+  by rewrite mathcomp_extra.lt_succ_floor.
 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.
@@ -157,10 +156,10 @@ 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 sumr_const -cardfE card_fseq undup_id // eq_si -mulr_natr -pmulrn.
-rewrite mul1r natrM mulrCA mulVf ?mulr1 ?pnatr_eq0 //.
-have /andP[_] := mem_rg1_floor M; rewrite -addn1.
-by rewrite natrD /= mulr1n pmulrn -{1}[Num.floor _]gez0_abs // floor_ge0.
+rewrite mul1r sumr_const -cardfE card_fseq undup_id // eq_si.
+rewrite -mulr_natr natrM mulrC mulfK ?pnatr_eq0//.
+rewrite pmulrn -addn1 PoszD gez0_abs ?floor_ge0//.
+by rewrite mathcomp_extra.lt_succ_floor.
 Qed.
 
 End SummableCountable.

theories/lebesgue_integral.v

@@ -1288,16 +1288,10 @@ Lemma bigsetU_dyadic_itv n : `[n%:R, n.+1%:R[%classic =
 Proof.
 rewrite predeqE => r; split => [/= /[!in_itv]/= /andP[nr rn1]|].
 - rewrite -bigcup_seq /=; exists `|floor (r * 2 ^+ n.+1)|%N.
-    rewrite /= mem_index_iota; apply/andP; split.
-      rewrite -ltez_nat gez0_abs ?floor_ge0; last first.
-        by rewrite mulr_ge0// (le_trans _ nr).
-      apply: (@le_trans _ _ (floor (n * 2 ^ n.+1)%:R)); last first.
-        by apply: floor_le; rewrite natrM natrX ler_pM2r.
-      by rewrite -floor_ge_int.
-    rewrite -ltz_nat gez0_abs; last first.
-      by rewrite floor_ge0 mulr_ge0// (le_trans _ nr).
-    rewrite -(@ltr_int R) (le_lt_trans (ge_floor _)) ?num_real//.
-    by rewrite PoszM intrM -natrX ltr_pM2r.
+    rewrite /= mem_index_iota -ltz_nat -lez_nat gez0_abs ?floor_ge0; last first.
+      by rewrite mulr_ge0// (le_trans _ nr).
+    rewrite -mathcomp_extra.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 _)) ?num_real//.
     by rewrite -(@gez0_abs (floor _))// floor_ge0 mulr_ge0// (le_trans _ nr).

theories/lebesgue_measure.v

@@ -1155,10 +1155,10 @@ rewrite [X in measurable X](_ : _ =
                           exact: emeasurable_fun_infty_c].
 rewrite predeqE => t; split => [/= [Dt ft]|].
   have [ft0|ft0] := leP 0%R (fine (f t)).
-    exists `|(ceil (fine (f t)))%real|%N => //=; split => //; split.
+    exists `|ceil (fine (f t))|%N => //=; split => //; split.
       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)))%real|%N => //=; split => //; split.
+  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.
   by rewrite -(fineK ft)// lee_fin (le_trans (ltW ft0)).
@@ -1403,7 +1403,7 @@ Lemma eset1Ny :
 Proof.
 rewrite eqEsubset; split=> [_ -> i _ |]; first by rewrite /= in_itv /= ltNyr.
 move=> [r|/(_ O Logic.I)|]//.
-move=> /(_ `|(floor r)%real|%N Logic.I); rewrite /= in_itv/= ltNge.
+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.
@@ -1414,7 +1414,7 @@ Qed.
 Lemma eset1y : [set +oo] = \bigcap_k `]k%:R%:E, +oo[%classic :> set (\bar R).
 Proof.
 rewrite eqEsubset; split=> [_ -> i _/=|]; first by rewrite in_itv /= ltry.
-move=> [r| |/(_ O Logic.I)] // /(_ `|(ceil r)%real|%N Logic.I); rewrite /= in_itv /=.
+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.
@@ -2400,7 +2400,7 @@ have {}EBr2 : \esum_(i in E) mu (closure (B i)) <=
   by apply: bigcup_measurable => *; exact: measurable_closure.
 have finite_set_F i : finite_set (F i).
   apply: contrapT.
-  pose M := `|(ceil ((r%:num + 2) *+ 2 / (1 / (2 ^ i.+1)%:R)))%real|.+1.
+  pose M := `|ceil ((r%:num + 2) *+ 2 / (1 / (2 ^ i.+1)%:R))|.+1.
   move/(infinite_set_fset M) => [/= C] CsubFi McardC.
   have MC : (M%:R * (1 / (2 ^ i.+1)%:R))%:E <=
             mu (\bigcup_(j in [set` C]) closure (B j)).

theories/lebesgue_stieltjes_measure.v

@@ -482,9 +482,9 @@ Lemma wlength_sigma_finite (f : R -> R) :
 Proof.
 exists (fun k => `](- k%:R), k%:R]%classic).
   apply/esym; rewrite -subTset => /= x _ /=.
-  exists `|((floor `|x|%R)%real + 1)%R|%N; rewrite //= in_itv/=.
+  exists `|(floor `|x| + 1)%R|%N; rewrite //= in_itv/=.
   rewrite !natr_absz intr_norm intrD.
-  suff: `|x| < `|(floor `|x|)%real%:~R + 1| by rewrite ltr_norml => /andP[-> /ltW->].
+  suff: `|x| < `|(floor `|x|)%:~R + 1| by rewrite ltr_norml => /andP[-> /ltW->].
   rewrite [ltRHS]ger0_norm//.
     by rewrite intr1 (le_lt_trans _ (lt_succ_floor _))// ?ler_norm.
   by rewrite addr_ge0// ler0z floor_ge0.