Fixed the infamous %E scope bug

CHANGELOG_UNRELEASED.md

@@ -71,6 +71,9 @@
   + lemmas `compact_EVT_max`, `compact_EVT_min`, `EVT_max_rV`, `EVT_min_rV`
 
 ### Changed
+
+- in `constructive_ereal.v`: fixed the infamous `%E` scope bug.
+
 - in set_interval.v
   + `setUitv1`, `setU1itv`, `setDitv1l`, `setDitv1r` (generalized)
 

experimental_reals/discrete.v

@@ -4,7 +4,7 @@
 (* Copyright (c) - 2016--2018 - Polytechnique                           *)
 
 (* -------------------------------------------------------------------- *)
-From Corelib Require Setoid.
+From Coq Require Setoid.
 From HB Require Import structures.
 From mathcomp Require Import all_ssreflect_compat all_algebra.
 From mathcomp.classical Require Import boolp.

reals/constructive_ereal.v

@@ -570,14 +570,63 @@ End ERealArith.
 Arguments mule : simpl never.
 Arguments inve : simpl never.
 
-Notation "+%dE"  := (@GRing.add (\bar^d _)).
-Notation "+%E"   := (@GRing.add (\bar _)).
-Notation "-%E"   := oppe.
-Notation "x + y" := (GRing.add (x%dE : \bar^d _) y%dE) : ereal_dual_scope.
-Notation "x + y" := (GRing.add x%E y%E) : ereal_scope.
-Notation "x - y" := ((x%dE : \bar^d _) + oppe y%dE) : ereal_dual_scope.
-Notation "x - y" := (x%E + (oppe y%E)) : ereal_scope.
-Notation "- x"   := (oppe x%dE : \bar^d _) : ereal_dual_scope.
+
+(* We use elpi to name the canonical nmodule for \bar R and \bar^d R. *)
+(* This used to be called `extended_nmodType` and `dual_extended_nmodType`. *)
+(* HB gives them generated names now, though we should restore naming cf *)
+(* https://github.com/math-comp/hierarchy-builder/issues/328 *)
+Elpi Command canonical_notation_ereal.
+Elpi Accumulate lp:{{
+      main [] :-
+        coq.unify-leq {{\bar lp:_}} {{GRing.Nmodule.sort lp:M}} ok,
+        coq.safe-dest-app M CR _,
+        coq.notation.add-abbreviation "extended_nmodType" 0 CR tt _.
+  }}.
+Elpi canonical_notation_ereal.
+Elpi Command canonical_notation_dual_ereal.
+Elpi Accumulate lp:{{
+      main [] :-
+        coq.unify-leq {{dual_extended lp:_}} {{GRing.Nmodule.sort lp:M}} ok,
+        coq.safe-dest-app M CR _,
+        coq.notation.add-abbreviation "dual_extended_nmodType" 0 CR tt _.
+  }}.
+Elpi canonical_notation_dual_ereal.
+
+(* We provide local notations for parsing and printing of particular *)
+(* instances of generic notations. *)
+Local Notation add_parsingde := (@GRing.add (\bar^d _)).
+Local Notation add_rcde := (@GRing.add (@reverse_coercion _ _ _ (\bar^d _))).
+Local Notation add_cande := (@GRing.add dual_extended_nmodType).
+Local Notation add_parsinge := (@GRing.add (\bar _)).
+Local Notation add_rce := (@GRing.add (@reverse_coercion _ _ _ (\bar _))).
+Local Notation add_cane := (@GRing.add extended_nmodType).
+
+Notation "+%dE" := add_parsingde (only parsing).
+Notation "+%dE" := add_rcde (only printing).
+Notation "+%dE" := add_cande (only printing).
+Notation "+%E"  := add_parsinge (only parsing).
+Notation "+%E"  := add_rce (only printing).
+Notation "+%E"  := add_cane (only printing).
+Notation "-%E"  := oppe.
+Notation "x + y" := (add_parsingde x%dE y%dE) (only parsing) : ereal_dual_scope.
+Notation "x + y" := (add_rcde x%dE y%dE) (only printing) : ereal_dual_scope.
+Notation "x + y" := (add_cande x%dE y%dE) (only printing) : ereal_dual_scope.
+Notation "x + y" := (add_parsinge x%E y%E) (only parsing) : ereal_scope.
+Notation "x + y" := (add_rce x%E y%E) (only printing) : ereal_scope.
+Notation "x + y" := (add_cane x%E y%E) (only printing) : ereal_scope.
+Notation "x - y" := (add_parsingde x%dE (oppe (y%dE : \bar^d _))%dE)
+  (only parsing) : ereal_dual_scope.
+Notation "x - y" := (add_rcde x%dE (oppe y%dE))
+  (only printing) : ereal_dual_scope.
+Notation "x - y" := (add_cande x%dE (oppe y%dE))
+  (only printing) : ereal_dual_scope.
+Notation "x - y" := (add_parsinge x%E (oppe y%E)) (only parsing) : ereal_scope.
+Notation "x - y" := (add_rce x%E (oppe y%E)) (only printing) : ereal_scope.
+Notation "x - y" := (add_cane x%E (oppe y%E)) (only printing) : ereal_scope.
+(* All previous notations should ideal by generated too, *)
+(* but elpi lacks support for string notations.          *)
+
+Notation "- x"   := (oppe (x%dE : \bar^d _)) : ereal_dual_scope.
 Notation "- x"   := (oppe x%E) : ereal_scope.
 Notation "*%E"   := mule.
 Notation "x * y" := (mule x%dE y%dE : \bar^d _) : ereal_dual_scope.
@@ -643,12 +692,23 @@ Notation "- 1" := (oppe 1) : ereal_scope.
 
 Notation "\- f" := (fun x => - f x)%dE : ereal_dual_scope.
 Notation "\- f" := (fun x => - f x)%E : ereal_scope.
-Notation "f \+ g" := (fun x => f x + g x)%dE : ereal_dual_scope.
-Notation "f \+ g" := (fun x => f x + g x)%E : ereal_scope.
-Notation "f \* g" := (fun x => f x * g x)%dE : ereal_dual_scope.
-Notation "f \* g" := (fun x => f x * g x)%E : ereal_scope.
-Notation "f \- g" := (fun x => f x - g x)%dE : ereal_dual_scope.
-Notation "f \- g" := (fun x => f x - g x)%E : ereal_scope.
+Notation "f \+ g" := (fun x => add_parsingde (f x)%dE (g x)%dE) (only parsing) : ereal_dual_scope.
+Notation "f \+ g" := (fun x => add_rcde (f x)%dE (g x)%dE) (only printing) : ereal_dual_scope.
+Notation "f \+ g" := (fun x => add_cande (f x)%dE (g x)%dE) (only printing) : ereal_dual_scope.
+Notation "f \+ g" := (fun x => add_parsinge (f x)%E (g x)%E) (only parsing) : ereal_scope.
+Notation "f \+ g" := (fun x => add_rce (f x)%E (g x)%E) (only printing) : ereal_scope.
+Notation "f \+ g" := (fun x => add_cane (f x)%E (g x)%E) (only printing) : ereal_scope.
+Notation "f \- g" := (fun x => add_parsingde ((f x)%dE : \bar^d _) (oppe ((g%dE x) : \bar^d _))%dE)
+  (only parsing) : ereal_dual_scope.
+Notation "f \- g" := (fun x => add_rcde (f x)%dE (oppe (g x)%dE))
+  (only printing) : ereal_dual_scope.
+Notation "f \- g" := (fun x => add_cande (f x)%dE (oppe (g x)%dE))
+  (only printing) : ereal_dual_scope.
+Notation "f \- g" := (fun x => add_parsinge ((f x)%E : \bar _) (oppe (g x)%E)) (only parsing) : ereal_scope.
+Notation "f \- g" := (fun x => add_rce (f x)%E (oppe (g x)%E)) (only printing) : ereal_scope.
+Notation "f \- g" := (fun x => add_cane (f x)%E (oppe (g x)%E)) (only printing) : ereal_scope.
+Notation "f \* g" := (fun x => (f x * g x)%dE) : ereal_dual_scope.
+Notation "f \* g" := (fun x => (f x * g x)%E) : ereal_scope.
 
 Notation "\sum_ ( i <- r | P ) F" :=
   (\big[+%dE/0%dE]_(i <- r | P%B) F%dE) : ereal_dual_scope.

theories/ess_sup_inf.v

@@ -217,11 +217,11 @@ Proof. by move=> ?; apply/ess_supP; apply: nearW. Qed.
 Lemma ess_sup_cstr y : 0 < mu [set: T] -> ess_supr (cst y) = y%:E.
 Proof. by move=> muN0; rewrite (ess_sup_ae_cst y%:E)//=; apply: nearW. Qed.
 
-Lemma ess_suprD f g : ess_supr (f \+ g) <= ess_supr f + ess_supr g.
+Lemma ess_suprD f g : ess_supr (f \+ g)%R <= ess_supr f + ess_supr g.
 Proof. by rewrite (le_trans _ (ess_supD _ _ _)). Qed.
 
 Lemma ess_sup_normD f g :
-  ess_supr (normr \o (f \+ g)) <= ess_supr (normr \o f) + ess_supr (normr \o g).
+  ess_supr (normr \o (f \+ g)%R) <= ess_supr (normr \o f) + ess_supr (normr \o g).
 Proof.
 rewrite (le_trans _ (ess_suprD _ _))// le_ess_sup//.
 by apply/nearW => x; apply/ler_normD.

theories/ftc.v

@@ -88,7 +88,7 @@ Qed.
 Let FTC0 f a : mu.-integrable setT (EFin \o f) ->
   let F x := (\int[mu]_(t in [set` Interval a (BRight x)]) f t)%R in
   forall x, a < BRight x -> lebesgue_pt f x ->
-    h^-1 *: (F (h + x) - F x) @[h --> 0%R^'] --> f x.
+    h^-1 *: (F (h + x)%R - F x) @[h --> 0%R^'] --> f x.
 Proof.
 move=> intf F x ax fx.
 have locf : locally_integrable setT f.
@@ -106,7 +106,7 @@ apply: cvg_at_right_left_dnbhs.
       by rewrite (lt_le_trans _ yz)// ltrBlDr ltrDl.
     rewrite (lebesgue_measure_ball _ (ltW _))// -/mu muE -EFinM lee_fin.
     by rewrite mulr_natl.
-  have ixdf n : \int[mu]_(t in [set` Interval a (BRight (x + d n))]) (f t)%:E -
+  have ixdf n : \int[mu]_(t in [set` Interval a (BRight (x + d n)%R)]) (f t)%:E -
                 \int[mu]_(t in [set` Interval a (BRight x)]) (f t)%:E =
                 \int[mu]_(y in E x n) (f y)%:E.
     rewrite -[in X in X - _]integral_itv_bndo_bndc; last first.
@@ -161,7 +161,7 @@ apply: cvg_at_right_left_dnbhs.
     rewrite lebesgue_measure_ball//; last exact: ltW.
     by rewrite -/mu muE -EFinM lee_fin mulr_natl.
   have ixdf : {near \oo,
-      (fun n => \int[mu]_(t in [set` Interval a (BRight (x + d n))]) (f t)%:E -
+      (fun n => \int[mu]_(t in [set` Interval a (BRight (x + d n)%R)]) (f t)%:E -
                 \int[mu]_(t in [set` Interval a (BRight x)]) (f t)%:E) =1
       (fun n => - (\int[mu]_(y in E x n) (f y)%:E))}.
     case: a ax {F}; last first.
@@ -236,7 +236,7 @@ Let FTC0_restrict f a x (u : R) : (x < u)%R ->
   mu.-integrable [set` Interval a (BRight u)] (EFin \o f) ->
   let F y := (\int[mu]_(t in [set` Interval a (BRight y)]) f t)%R in
   a < BRight x -> lebesgue_pt f x ->
-  h^-1 *: (F (h + x) - F x) @[h --> 0%R^'] --> f x.
+  h^-1 *: (F (h + x)%R - F x) @[h --> 0%R^'] --> f x.
 Proof.
 move=> xu + F ax fx.
 rewrite integrable_mkcond//= (restrict_EFin f) => intf.
@@ -270,7 +270,7 @@ have /= := FTC0_restrict xu intf ax fx.
 set g := (f in f n @[n --> _] --> _ -> _).
 set h := (f in _ -> f n @[n --> _] --> _).
 suff : g = h by move=> <-.
-by apply/funext => y;rewrite /g /h /= [X in F (X + _)]mulr1.
+by apply/funext => y;rewrite /g /h /= [X in F (X + _)%R]mulr1.
 Qed.
 
 Corollary FTC1 f a :
@@ -606,7 +606,7 @@ have GacFa : G x @[x --> a^'+] --> (- c + F a)%R.
     rewrite opprB GFc; last by rewrite in_itv/=; apply/andP.
     by rewrite addNr normr0 ltW.
   have := @cvgD _ _ _ _ Fap _ _ _ _ GFac Fa.
-  rewrite (_ : (G \- F)%R + F = G)//.
+  rewrite (_ : (G \- F) + F = G)%R//.
   by apply/funext => x/=; rewrite subrK.
 have GbcFb : G x @[x --> b^'-] --> (- c + F b)%R.
   have Fbn : Filter b^'- by exact: at_left_proper_filter.
@@ -615,7 +615,7 @@ have GbcFb : G x @[x --> b^'-] --> (- c + F b)%R.
     rewrite opprB GFc; last by rewrite in_itv/=; apply/andP.
     by rewrite addNr normr0 ltW.
   have := @cvgD _ _ _ _ Fbn _ _ _ _ GFbc Fb.
-  rewrite (_ : (G \- F)%R + F = G)//.
+  rewrite (_ : G \- F + F = G)%R //.
   by apply/funext => x/=; rewrite subrK.
 have contF : {within `[a, b], continuous F}.
   apply/(continuous_within_itvP _ ab); split => //.
@@ -661,18 +661,18 @@ rewrite ge0_integral_bigcup//=; last 3 first.
 - by rewrite -seqDU_bigcup_eq -itv_bndy_bigcup_BRight; exact: measurableT_comp.
 - move=> x/=; rewrite -seqDU_bigcup_eq -itv_bndy_bigcup_BRight/=.
   by rewrite /= in_itv/= => /andP[/ltW + _]; rewrite lee_fin; exact: f_ge0.
-have dFEn n : {in `]a + n%:R, a + n.+1%:R[, F^`() =1 f}.
+have dFEn n : {in `](a + n%:R)%R, (a + n.+1%:R)%R[, F^`() =1 f}.
   apply: in1_subset_itv dFE.
   apply: subset_trans (subset_itvl _) (subset_itvr _) => //=.
   by rewrite bnd_simp lerDl.
-have liml : limn (EFin \o (fun k => F (a + k%:R))) = l%:E.
+have liml : limn (EFin \o (fun k => F (a + k%:R)%R)) = l%:E.
   apply/cvg_lim => //.
   apply: cvg_EFin; first exact: nearW.
   apply/((cvg_pinftyP F l).1 Fxl)/cvgryPge => r.
   by near do rewrite -lerBlDl; exact: nbhs_infty_ger.
 transitivity (\sum_(0 <= i <oo) ((F (a + i.+1%:R))%:E - (F (a + i%:R))%:E)).
   transitivity (\sum_(0 <= i <oo)
-      \int[mu]_(x in seqDU (fun k => `]a, (a + k%:R)]%classic) i.+1) (f x)%:E).
+      \int[mu]_(x in seqDU (fun k => `]a, (a + k%:R)%R]%classic) i.+1) (f x)%:E).
     apply/cvg_lim => //; rewrite -cvg_shiftS/=.
     under eq_cvg.
       move=> k /=; rewrite big_nat_recl//.
@@ -700,13 +700,13 @@ transitivity (\sum_(0 <= i <oo) ((F (a + i.+1%:R))%:E - (F (a + i%:R))%:E)).
     + move=> x; rewrite in_itv/= => /andP[anx _].
       by apply/dF; rewrite (le_lt_trans _ anx)// lerDl.
     + move: n => [|n]; first by rewrite addr0.
-      have : {within `[a + n.+1%:R, a + n.+2%:R], continuous F}.
+      have : {within `[(a + n.+1%:R)%R, (a + n.+2%:R)%R], continuous F}.
         apply: derivable_within_continuous => /= x.
         rewrite in_itv/= => /andP[aSn _].
         by apply: dF; rewrite (lt_le_trans _ aSn)// ltrDl.
       move/continuous_within_itvP.
       by rewrite ltrD2l ltr_nat ltnS => /(_ (ltnSn _))[].
-  - have : {within `[a + n%:R + 2^-1%R, a + n.+1%:R], continuous F}.
+  - have : {within `[(a + n%:R + 2^-1%R)%R, (a + n.+1%:R)%R], continuous F}.
       apply: derivable_within_continuous => x.
       rewrite in_itv/= => /andP[aSn _].
       by apply: dF; rewrite (lt_le_trans _ aSn)// -addrA ltrDl ltr_wpDl.
@@ -717,7 +717,7 @@ rewrite nondecreasing_telescope_sumey.
 - by rewrite addr0 EFinN; congr (_ - _).
 - by rewrite liml.
 - apply/nondecreasing_seqP => n; rewrite -subr_ge0.
-  have isdF (x : R) : x \in `]a + n%:R, a + n.+1%:R[ -> is_derive x 1%R F (f x).
+  have isdF (x : R) : x \in `](a + n%:R)%R, (a + n.+1%:R)%R[ -> is_derive x 1%R F (f x).
     rewrite in_itv/= => /andP[anx _].
     rewrite -dFE; last by rewrite in_itv/= andbT (le_lt_trans _ anx)// lerDl.
     rewrite derive1E.
@@ -1283,12 +1283,12 @@ Lemma decreasing_ge0_integration_by_substitutiony F G a :
 Proof.
 move=> decrF cdF /cvg_ex[/= dFa cdFa] /cvg_ex[/= dFoo cdFoo].
 move=> [dF cFa] Fny /continuous_within_itvNycP[cG cGFa] G0.
-have mG n : measurable_fun `](F (a + n.+1%:R)), (F a)] G.
+have mG n : measurable_fun `](F (a + n.+1%:R)%R), (F a)] G.
   apply/measurable_fun_itv_bndo_bndcP.
   apply: open_continuous_measurable_fun; first exact: interval_open.
   move=> x; rewrite inE/= in_itv/= => /andP[_ xFa].
   by apply: cG; rewrite in_itv.
-have mGFNF' i : measurable_fun `[a, (a + i.+1%:R)[ ((G \o F) * - F^`())%R.
+have mGFNF' i : measurable_fun `[a, (a + i.+1%:R)%R[ ((G \o F) * - F^`())%R.
   apply/measurable_fun_itv_obnd_cbndP.
   apply: open_continuous_measurable_fun; first exact: interval_open.
   move=> x; rewrite inE/= in_itv/= => /andP[ax _].
@@ -1330,15 +1330,15 @@ transitivity (limn (fun n => \int[mu]_(x in `[F (a + n%:R)%R, F a[) (G x)%:E)).
     apply: G0.
     move: xFaSkFa.
     rewrite big_mkord -bigsetU_seqDU.
-    rewrite -(bigcup_mkord _ (fun k => `]F (a + k.+1%:R), F a[%classic)).
+    rewrite -(bigcup_mkord _ (fun k => `]F (a + k.+1%:R)%R, F a[%classic)).
     by move: x; apply: bigcup_sub => k/= nk; exact: subset_itvr.
   rewrite -integral_itv_obnd_cbnd; last first.
     apply/measurable_EFinP; case: n => [|n].
       by rewrite addr0 set_itvoo0; exact: measurable_fun_set0.
     by apply: measurable_funS (mG n) => //; exact: subset_itvW.
   congr (integral _).
   rewrite big_mkord -bigsetU_seqDU.
-  rewrite -(bigcup_mkord _ (fun k => `]F (a + k.+1%:R), F a[%classic)).
+  rewrite -(bigcup_mkord _ (fun k => `]F (a + k.+1%:R)%R, F a[%classic)).
   exact/esym/decreasing_itvoo_bigcup.
 transitivity (limn (fun n =>
     \int[mu]_(x in `]a, (a + n%:R)%R[) (((G \o F) * - F^`()) x)%:E)); last first.
@@ -1375,15 +1375,15 @@ transitivity (limn (fun n =>
   - exact: iota_uniq.
   - exact: (@sub_trivIset _ _ _ [set: nat]).
   - apply/measurable_EFinP.
-    apply: (measurable_funS (measurable_itv `]a, (a + n.+1%:R)[)).
+    apply: (measurable_funS (measurable_itv `]a, (a + n.+1%:R)%R[)).
       rewrite big_mkord -bigsetU_seqDU.
-      rewrite -(bigcup_mkord _ (fun k => `]a, (a + k.+1%:R)[%classic)).
+      rewrite -(bigcup_mkord _ (fun k => `]a, (a + k.+1%:R)%R[%classic)).
       apply: bigcup_sub => k/= kn.
       by apply: subset_itvl; rewrite bnd_simp/= lerD2l ler_nat ltnS ltnW.
     by apply: measurable_funS (mGFNF' n) => //; exact: subset_itv_oo_co.
   congr (integral _).
   rewrite big_mkord -bigsetU_seqDU.
-  rewrite -(bigcup_mkord n (fun k => `]a, (a + k.+1%:R)[%classic)).
+  rewrite -(bigcup_mkord n (fun k => `]a, (a + k.+1%:R)%R[%classic)).
   rewrite eqEsubset; split.
     move: n => [|n]; first by rewrite addr0 set_itvoo0.
     by apply: (@bigcup_sup _ _ n) => /=.

theories/gauss_integral.v

@@ -170,7 +170,7 @@ by rewrite expr0n/= oppr0 expR0 gauss_fun_le1.
 Unshelve. all: end_near. Qed.
 
 Let cvg_dintegral01_u x :
-  h^-1 *: (integral01_u (h + x)%E - integral01_u x) @[h --> 0^'] -->
+  h^-1 *: (integral01_u (h + x) - integral01_u x) @[h --> 0^'] -->
   - 2 * x * gauss_fun x * \int[mu]_(t in `[0, 1]) gauss_fun (t * x).
 Proof.
 have [c [e e0 cex]] : exists c : R, exists2 e : R, 0 < e & ball c e x.

theories/hoelder.v

@@ -742,7 +742,7 @@ Qed.
 
 Lemma lerB_DLnorm f g p :
   measurable_fun [set: T] f -> measurable_fun [set: T] g -> (1 <= p)%R ->
-  'N_p%:E[f] <= 'N_p%:E[f \+ g] + 'N_p%:E[g].
+  'N_p%:E[f] <= 'N_p%:E[(f \+ g)%R] + 'N_p%:E[g].
 Proof.
 move=> mf mg p1.
 rewrite [in leLHS](_ : f = ((f + g) + (-%R \o g))%R); last by rewrite addrK.
@@ -756,7 +756,7 @@ Qed.
 
 Lemma lerB_LnormD f g p :
   measurable_fun [set: T] f -> measurable_fun [set: T] g -> (1 <= p)%R ->
-  'N_p%:E[f] - 'N_p%:E[g] <= 'N_p%:E[f \+ g].
+  'N_p%:E[f] - 'N_p%:E[g] <= 'N_p%:E[(f \+ g)%R].
 Proof.
 move=> mf mg p1.
 set rhs := (leRHS); have [?|] := boolP (rhs \is a fin_num).

theories/probability_theory/random_variable.v

@@ -303,7 +303,7 @@ Qed.
 Lemma cdf_right_continuous : right_continuous (cdf X).
 Proof.
 move=> a.
-pose s := fine (ereal_inf (cdf X @` `]a, a + 1%R]%classic)).
+pose s := fine (ereal_inf (cdf X @` `]a, (a + 1)%R]%classic)).
 have cdf_s : cdf X r @[r --> a^'+] --> s%:E.
   rewrite /s fineK.
   - apply: nondecreasing_at_right_cvge; first by rewrite ltBSide /= ?ltrDl.
@@ -312,13 +312,13 @@ have cdf_s : cdf X r @[r --> a^'+] --> s%:E.
     + by rewrite (lt_le_trans (ltNyr 0%R)) ?le_ereal_inf_tmp//= => l[? _] <-.
     + rewrite (le_lt_trans _ (ltry 1%R))// ge_ereal_inf//=.
       exists (cdf X (a + 1)); last exact: cdf_le1.
-      by exists (a + 1%R) => //; rewrite in_itv /=; apply/andP; rewrite ltrDl.
+      by exists (a + 1)%R => //; rewrite in_itv /=; apply/andP; rewrite ltrDl.
 have cdf_ns : cdf X (a + n.+1%:R^-1) @[n --> \oo] --> s%:E.
   move/cvge_at_rightP : cdf_s; apply; split=> [n|]; rewrite ?ltrDl //.
   rewrite -[X in _ --> X]addr0; apply: (@cvgD _ R^o); first exact: cvg_cst.
   by rewrite gtr0_cvgV0 ?cvg_shiftS; [exact: cvgr_idn | near=> n].
 have cdf_na : cdf X (a + n.+1%:R^-1) @[n --> \oo] --> cdf X a.
-  pose F n := X @^-1` `]-oo, a + n.+1%:R^-1%R].
+  pose F n := X @^-1` `]-oo, (a + n.+1%:R^-1)%R].
   suff : P (F n) @[n --> \oo] --> P (\bigcap_n F n).
     by rewrite [in X in _ --> X -> _]/F -preimage_bigcap -itvNycEbigcap.
   apply: nonincreasing_cvg_mu => [| | |m n mn].

theories/realfun.v

@@ -2042,7 +2042,7 @@ by move/hasNub_ereal_sup; apply; exact: variations_neq0.
 Qed.
 
 Lemma total_variation_le a b f g : a <= b ->
-  (TV a b (f \+ g) <= TV a b f + TV a b g)%E.
+  (TV a b (f \+ g)%R <= TV a b f + TV a b g)%E.
 Proof.
 rewrite le_eqVlt => /predU1P[<-{b}|ab].
   by rewrite !total_variationxx adde0.

theories/sequences.v

@@ -1478,14 +1478,14 @@ have <- : sup (range v_) = fine l.
     by exists (m + N)%N => //; rewrite /v_/= fineK// u_fin_num// leq_addl.
   apply: ge_ereal_sup => /= _ [m _] <-.
   rewrite (@le_trans _ _ (u_ (m + N)%N))//; first by rewrite nd_u_// leq_addr.
-  apply: ereal_sup_ubound => /=; exists (fine (u_ (m + N))); first by exists m.
+  apply: ereal_sup_ubound => /=; exists (fine (u_ (m + N)%N)); first by exists m.
   by rewrite fineK// u_fin_num// leq_addl.
 apply: nondecreasing_cvgn.
 - move=> m n mn /=; rewrite /v_ /= fine_le ?u_fin_num ?leq_addl//.
   by rewrite nd_u_// leq_add2r.
 - exists (fine l) => /= _ [m _ <-]; rewrite /v_ /= fine_le//.
     by rewrite u_fin_num// leq_addl.
-  by apply: ereal_sup_ubound; exists (m + N).
+  by apply: ereal_sup_ubound; exists (m + N)%N.
 Unshelve. all: by end_near. Qed.
 
 Lemma ereal_nondecreasing_is_cvgn (R : realType) (u_ : (\bar R) ^nat) :