adapt to mc#1256

altreals/realseq.v

@@ -303,7 +303,7 @@ Lemma ncvgM u v lu lv : ncvg u lu%:E -> ncvg v lv%:E ->
 Proof.
 move=> cu cv; pose a := u \- lu%:S; pose b := v \- lv%:S.
 have eq: (u \* v) =1 (lu * lv)%:S \+ ((lu%:S \* b) \+ (a \* v)).
-  move=> n; rewrite {}/a {}/b /= [u n+_]addrC [(_+_)*(v n)]mulrDl.
+  move=> n; rewrite {}/a {}/b /= [(u + _) n]addrC [(_+_)*(v n)]mulrDl.
   rewrite !addrA -[LHS]add0r; congr (_ + _); rewrite mulrDr.
   by rewrite !(mulrN, mulNr) (addrCA (lu * lv)) subrr addr0 subrr.
 apply/(ncvg_eq eq); rewrite -[X in X%:E]addr0; apply/ncvgD.

classical/cardinality.v

@@ -1340,7 +1340,7 @@ Section zmod.
 Context (aT : Type) (rT : zmodType).
 Lemma fimfun_zmod_closed : zmod_closed (@fimfun aT rT).
 Proof.
-split=> [|f g]; rewrite !inE/=; first exact: finite_image_cst.
+split=> [|f g]; rewrite !inE/=; first exact: (finite_image_cst 0).
 by move=> fA gA; apply: (finite_image11 (fun x y => x - y)).
 Qed.
 HB.instance Definition _ :=

reals/constructive_ereal.v

@@ -137,7 +137,7 @@ Definition er_map T T' (f : T -> T') (x : \bar T) : \bar T' :=
 Lemma er_map_idfun T (x : \bar T) : er_map idfun x = x.
 Proof. by case: x. Qed.
 
-Definition fine {R : zmodType} x : R := if x is EFin v then v else 0.
+Definition fine {R : zmodType} x : R := if x is EFin v then v else 0%R.
 
 Section EqEReal.
 Variable (R : eqType).

theories/derive.v

@@ -253,12 +253,12 @@ Lemma derivable_nbhs (f : V -> W) a v :
 Proof.
 move=> df; apply/eqaddoP => _/posnumP[e].
 rewrite -nbhs_nearE nbhs_simpl /= dnbhsE; split; last first.
-  rewrite /at_point opprD -![(_ + _ : _ -> _) _]/(_ + _) scale0r add0r.
+  rewrite /at_point opprD !GRing.add_funE !GRing.opp_funE scale0r add0r.
   by rewrite addrA subrr add0r normrN scale0r !normr0 mulr0.
 have /eqolimP := df.
 move=> /eqaddoP /(_ e%:num) /(_ [gt0 of e%:num]).
 apply: filter_app; rewrite /= !near_simpl near_withinE; near=> h => hN0.
-rewrite /= opprD -![(_ + _ : _ -> _) _]/(_ + _) -![(- _ : _ -> _) _]/(- _).
+rewrite /= opprD !GRing.add_funE !GRing.opp_funE.
 rewrite /cst /= [`|1|]normr1 mulr1 => dfv.
 rewrite addrA -[X in X + _]scale1r -(@mulVf _ h) //.
 rewrite mulrC -scalerA -scalerBr normrZ.
@@ -276,7 +276,7 @@ move=> df; apply/cvg_ex; exists ('D_v f a).
 apply/(@eqolimP _ _ _ (dnbhs_filter_on _))/eqaddoP => _/posnumP[e].
 have /eqaddoP /(_ e%:num) /(_ [gt0 of e%:num]) := df.
 rewrite /= !(near_simpl, near_withinE); apply: filter_app; near=> h.
-rewrite /= opprD -![(_ + _ : _ -> _) _]/(_ + _) -![(- _ : _ -> _) _]/(- _).
+rewrite /= opprD !GRing.add_funE !GRing.opp_funE.
 rewrite /cst /= [`|1|]normr1 mulr1 addrA => dfv hN0.
 rewrite -[X in _ - X]scale1r -(@mulVf _ h) //.
 rewrite -scalerA -scalerBr normrZ normfV ler_pdivrMl ?normr_gt0 //.
@@ -398,7 +398,7 @@ Variable R : numFieldType.
 Fact dcst (V W : normedModType R) (a : W) (x : V) : continuous (0 : V -> W) /\
   cst a \o shift x = cst (cst a x) + \0 +o_ 0 id.
 Proof.
-split; first exact: cst_continuous.
+split; first exact: (@cst_continuous _ _ 0).
 apply/eqaddoE; rewrite addr0 funeqE => ? /=; rewrite -[LHS]addr0; congr (_ + _).
 by rewrite littleoE; last exact: littleo0_subproof.
 Qed.
@@ -531,7 +531,8 @@ have hdf h : (f \o shift x = cst (f x) + h +o_ 0 id) ->
   by apply/eqP; rewrite eq_sym addrC addr_eq0 oppo.
 rewrite (hdf _ dxf).
 suff /diff_locally /hdf -> : differentiable f x.
-  by rewrite opprD addrCA -(addrA (_ - _)) addKr oppox addox.
+  rewrite opprD addrCA -(addrA (_ - _)) addKr GRing.add_funE GRing.opp_funE.
+  by rewrite oppox addox.
 apply/diffP => /=.
 apply: (@getPex _ (fun (df : {linear V -> W}) => continuous df /\
   forall y, f y = f (lim (nbhs x)) + df (y - lim (nbhs x))
@@ -576,7 +577,8 @@ Qed.
 Lemma differentiable_sum n (f : 'I_n -> V -> W) (x : V) :
   (forall i, differentiable (f i) x) -> differentiable (\sum_(i < n) f i) x.
 Proof.
-by elim/big_ind : _ => // ? ? g h ?; apply: differentiableD; [exact:g|exact:h].
+elim/big_ind : _ => //[_|? ? g h ?]; first exact/(@differentiable_cst _ 0).
+apply: differentiableD; [exact:g|exact:h].
 Qed.
 
 Lemma diffN (f : V -> W) x :
@@ -1152,7 +1154,8 @@ Global Instance is_derive_sum n (h : 'I_n -> V -> W) (x v : V)
   (dh : 'I_n -> W) : (forall i, is_derive x v (h i) (dh i)) ->
   is_derive x v (\sum_(i < n) h i) (\sum_(i < n) dh i).
 Proof.
-by elim/big_ind2 : _ => // [|] *; [exact: is_derive_cst|exact: is_deriveD].
+by elim/big_ind2 : _ => // [|] *;
+    [exact: (@is_derive_cst _ _ _ 0)|exact: is_deriveD].
 Qed.
 
 Lemma derivable_sum n (h : 'I_n -> V -> W) (x v : V) :
@@ -1573,7 +1576,7 @@ have gcont : {within `[a, b], continuous g}.
   move=> x; apply: continuousD _ ; first by move=>?; exact: fcont.
   by apply/continuousN/continuous_subspaceT=> ?; exact: scalel_continuous.
 have gaegb : g a = g b.
-  rewrite /g -![(_ - _ : _ -> _) _]/(_ - _).
+  rewrite /g !GRing.add_funE !GRing.opp_funE.
   apply/eqP; rewrite -subr_eq /= opprK addrAC -addrA -scalerBl.
   rewrite [_ *: _]mulrA mulrC mulrA mulVf.
     by rewrite mul1r addrCA subrr addr0.

theories/esum.v

@@ -589,7 +589,8 @@ near=> n.
 rewrite distrC subr0.
 have -> : (C_ = A_ \- B_)%R.
   apply/funext => k.
-  rewrite /= /A_ /C_ /B_ -sumrN -big_split/= -summable_fine_sum//.
+  rewrite /= /A_ /C_ /B_ GRing.add_funE GRing.opp_funE.
+  rewrite -sumrN -big_split/= -summable_fine_sum//.
   apply eq_bigr => i Pi; rewrite -fineB//.
   - by rewrite [in LHS](funeposneg f).
   - by rewrite fin_num_abs (@summable_pinfty _ _ P) //; exact/summable_funepos.

theories/ftc.v

@@ -839,7 +839,8 @@ set f  := fun x => if x == a then r else if x == b then l else F^`() x.
 have fE : {in `]a, b[, F^`() =1 f}.
   by move=> x; rewrite in_itv/= => /andP[ax xb]; rewrite /f gt_eqF// lt_eqF.
 have DPGFE : {in `]a, b[, (- (PG \o F))%R^`() =1 ((G \o F) * (- f))%R}.
-  move=> x /[dup]xab /andP[ax xb]; rewrite derive1_comp //; last first.
+  move=> x /[dup]xab /andP[ax xb].
+  rewrite (derive1_comp (g:[email protected] R)) //; last first.
     apply: diff_derivable; apply: differentiable_comp; apply/derivable1_diffP.
       by case: Fab => + _ _; exact.
     by case: PGFbFa => + _ _; apply; exact: decreasing_image_oo.
@@ -886,7 +887,8 @@ rewrite oppeD//= -(continuous_FTC2 ab _ _ DPGFE); last 2 first.
 - have [/= dF rF lF] := Fab.
   have := derivable_oo_continuous_bnd_within PGFbFa.
   move=> /(continuous_within_itvP _ FbFa)[_ PGFb PGFa]; split => /=.
-  - move=> x xab; apply/derivable1_diffP; apply: differentiable_comp => //.
+- move=> x xab; apply/derivable1_diffP.
+  apply: (differentiable_comp (g:[email protected] R)) => //.
     apply: differentiable_comp; apply/derivable1_diffP.
       by case: Fab => + _ _; exact.
     by case: PGFbFa => + _ _; apply; exact: decreasing_image_oo.
@@ -909,7 +911,7 @@ rewrite oppeD//= -(continuous_FTC2 ab _ _ DPGFE); last 2 first.
     rewrite gtr0_norm// ?subr_gt0//.
     by near: t; exact: nbhs_left_ltBl.
 apply: eq_integral_itv_bounded.
-- rewrite mulrN; apply: measurableT_comp => //.
+  - rewrite mulrN; apply: (measurableT_comp (f:[email protected] R)) => //.
   apply: (eq_measurable_fun ((G \o F) * F^`())%R) => //.
     by move=> x; rewrite inE/= => xab; rewrite !fctE fE.
   by move: mGFF'; apply: measurable_funS => //; exact: subset_itv_oo_cc.
@@ -994,13 +996,14 @@ have mF' : measurable_fun `]a, b[ F^`().
   apply: subspace_continuous_measurable_fun => //.
   by apply: continuous_in_subspaceT => x /[!inE] xab; exact: cF'.
 rewrite integral_itv_bndoo//; last first.
-  rewrite compA -(compA G -%R) (_ : -%R \o -%R = id); last first.
+  rewrite (compA _ -%R) -(compA G -%R) (_ : -%R \o -%R = id); last first.
     by apply/funext => y; rewrite /= opprK.
-  apply: measurable_funM => //; apply: measurableT_comp => //.
+  apply: measurable_funM => //.
+  apply: (measurableT_comp (f:[email protected] R)) => //.
   apply: (@eq_measurable_fun _ _ _ _ _ (- F^`())%R).
     move=> x /[!inE] xab; rewrite [in RHS]derive1E deriveN -?derive1E//.
     by case: Fab => + _ _; apply.
-  exact: measurableT_comp.
+  exact: (measurableT_comp (f:[email protected] R)).
 rewrite [in RHS]integral_itv_bndoo//; last exact: measurable_funM.
 apply: eq_integral => x /[!inE] xab; rewrite !fctE !opprK derive1E deriveN.
 - by rewrite opprK -derive1E.

theories/landau.v

@@ -414,7 +414,7 @@ Proof. by rewrite [RHS]littleoE. Qed.
 
 Lemma oppox (F : filter_on T) (f : T -> V) e x :
   - [o_F e of f] x = [o_F e of - [o_F e of f]] x.
-Proof. by move: x; rewrite -/(- _ =1 _) {1}oppo. Qed.
+Proof. by move: x; rewrite -/(- [o_F e of f] =1 _) {1}oppo. Qed.
 
 Lemma eqadd_some_oP (F : filter_on T) (f g : T -> V) (e : T -> W) h :
   f = g + [o_F e of h] -> littleo_def F (f - g) e.
@@ -596,7 +596,7 @@ Proof. by rewrite [RHS]bigOE. Qed.
 
 Lemma oppOx (F : filter_on T) (f : T -> V) e x :
   - [O_F e of f] x = [O_F e of - [O_F e of f]] x.
-Proof. by move: x; rewrite -/(- _ =1 _) {1}oppO. Qed.
+Proof. by move: x; rewrite -/(- [O_F e of f] =1 _) {1}oppO. Qed.
 
 Lemma add_bigO_subproof (F : filter_on T) e (df dg : {O_F e}) :
   bigO_def F (df \+ dg) e.
@@ -618,7 +618,7 @@ Proof. by rewrite [RHS]bigOE. Qed.
 Lemma addOx (F : filter_on T) (f g: T -> V) e x :
   [O_F e of f] x + [O_F e of g] x =
   [O_F e of [O_F e of f] + [O_F e of g]] x.
-Proof. by move: x; rewrite -/(_ + _ =1 _) {1}addO. Qed.
+Proof. by move: x; rewrite -/([O_F e of f] + _ =1 _) {1}addO. Qed.
 
 Lemma eqadd_some_OP (F : filter_on T) (f g : T -> V) (e : T -> W) h :
   f = g + [O_F e of h] -> bigO_def F (f - g) e.
@@ -848,7 +848,7 @@ Proof. by rewrite [RHS]littleoE. Qed.
 Lemma addox (F : filter_on T) (f g: T -> V) (e : _ -> W) x :
   [o_F e of f] x + [o_F e of g] x =
   [o_F e of [o_F e of f] + [o_F e of g]] x.
-Proof. by move: x; rewrite -/(_ + _ =1 _) {1}addo. Qed.
+Proof. by move: x; rewrite -/([o_F e of f] + _ =1 _) {1}addo. Qed.
 
 (* duplicate from Section Domination *)
 Hint Extern 0 (littleo_def _ _ _) => solve[apply: littleoP] : core.

theories/lebesgue_integral.v

@@ -5991,7 +5991,8 @@ Qed.
 Lemma locally_integrableN D f :
   locally_integrable D f -> locally_integrable D (\- f)%R.
 Proof.
-move=> [mf oD foo]; split => //; first exact: measurableT_comp.
+move=> [mf oD foo]; split => //.
+  exact: (measurableT_comp (f:[email protected] R)).
 by move=> K KD cK; under eq_integral do rewrite normrN; exact: foo.
 Qed.
 
@@ -6482,10 +6483,10 @@ Proof.
 move=> xU mU mUf cg locg; apply/eqP; rewrite eq_le; apply/andP; split.
 - rewrite [leRHS](_ : _ = f^* x + (\- g)%R^* x).
     apply: (lim_sup_davg_le xU) => //.
-    apply/(measurable_comp measurableT) => //.
+    apply/(measurable_comp (f:[email protected] R) measurableT) => //.
     by case: locg => + _ _; exact: measurable_funS.
   rewrite (@continuous_lim_sup_davg (- g)%R _ _ xU mU); first by rewrite adde0.
-  - apply/(measurable_comp measurableT) => //.
+  - apply/(measurable_comp (f:[email protected] R) measurableT) => //.
     by case: locg => + _ _; apply: measurable_funS.
   + by move=> y; exact/continuousN/cg.
 - rewrite [leRHS](_ : _ = ((f \- g)%R^* \+ g^*) x)//.
@@ -6870,8 +6871,9 @@ have HL_null n : mu (HLf_g_Be n) <= (3 / (e / 2))%:E * n.+1%:R^-1%:E.
   set h := (fun x => `|(f_ k \- g_ n) x|%:E) \_ (B k).
   rewrite (@eq_integral _ _ _ mu setT h)//=.
     by rewrite -integral_mkcond/=; exact: ifg_ub.
-  move=> x _; rewrite /h restrict_EFin restrict_normr/= /g_B /f_ !patchE.
-  by case: ifPn => /=; [rewrite patchE => ->|rewrite subrr].
+  move=> x _; rewrite /h restrict_EFin restrict_normr/= /g_B /f_/=.
+  rewrite GRing.sub_funE !patchE.
+  by case: ifPn => /=; [rewrite GRing.sub_funE patchE => ->|rewrite subrr].
 have fgn_null n : mu [set x | `|(f_ k \- g_B n) x|%:E >= (e / 2)%:E] <=
                      (e / 2)^-1%:E * n.+1%:R^-1%:E.
   rewrite lee_pdivlMl ?invr_gt0 ?divr_gt0// -[X in mu X]setTI.
@@ -6883,8 +6885,9 @@ have fgn_null n : mu [set x | `|(f_ k \- g_B n) x|%:E >= (e / 2)%:E] <=
   set h := (fun x => `|(f_ k \- g_ n) x|%:E) \_ (B k).
   rewrite (@eq_integral _ _ _ mu setT h)//=.
     by rewrite -integral_mkcond/=; exact: ifg_ub.
-  move=> x _; rewrite /h restrict_EFin restrict_normr/= /g_B /f_ !patchE.
-  by case: ifPn => /=; [rewrite patchE => ->|rewrite subrr].
+  move=> x _; rewrite /h restrict_EFin restrict_normr/= /g_B /f_/=.
+  rewrite GRing.sub_funE !patchE.
+  by case: ifPn => /=; [rewrite GRing.sub_funE patchE => ->|rewrite subrr].
 apply/eqP; rewrite eq_le measure_ge0 andbT.
 apply/lee_addgt0Pr => r r0; rewrite add0e.
 have incl n : Ee `<=` B k `&` (HLf_g_Be n `|` f_g_Be n) by move=> ?; apply.

theories/lebesgue_measure.v

@@ -1001,22 +1001,27 @@ by rewrite ltrBlDr=> afg; rewrite (lt_le_trans afg)// addrC lerD2r ltW.
 Qed.
 
 Lemma measurable_funB D f g : measurable_fun D f ->
-  measurable_fun D g -> measurable_fun D (f \- g).
-Proof. by move=> ? ?; apply: measurable_funD =>//; exact: measurableT_comp. Qed.
+  measurable_fun D g -> measurable_fun D (f - g).
+Proof.
+move=> ? ?; apply: measurable_funD =>//.
+exact: (measurableT_comp (f:[email protected] R)).
+Qed.
 
 Lemma measurable_funM D f g :
-  measurable_fun D f -> measurable_fun D g -> measurable_fun D (f \* g).
+  measurable_fun D f -> measurable_fun D g -> measurable_fun D (f * g).
 Proof.
-move=> mf mg; rewrite (_ : (_ \* _) = (fun x => 2%:R^-1 * (f x + g x) ^+ 2)
-  \- (fun x => 2%:R^-1 * (f x ^+ 2)) \- (fun x => 2%:R^-1 * (g x ^+ 2))).
+move=> mf mg.
+rewrite (_ : (_ * _) = (fun x => 2%:R^-1 * (f x + g x) ^+ 2)
+  - (fun x => 2%:R^-1 * (f x ^+ 2)) - (fun x => 2%:R^-1 * (g x ^+ 2))).
   apply: measurable_funB; first apply: measurable_funB.
   - apply: measurableT_comp => //.
     by apply: measurableT_comp (exprn_measurable _) _; exact: measurable_funD.
   - apply: measurableT_comp => //.
     exact: measurableT_comp (exprn_measurable _) _.
   - apply: measurableT_comp => //.
     exact: measurableT_comp (exprn_measurable _) _.
-rewrite funeqE => x /=; rewrite -2!mulrBr sqrrD (addrC (f x ^+ 2)) -addrA.
+rewrite funeqE => x /=.
+rewrite !GRing.sub_funE -2!mulrBr sqrrD (addrC (f x ^+ 2)) -addrA.
 rewrite -(addrA (f x * g x *+ 2)) -opprB opprK (addrC (g x ^+ 2)) addrK.
 by rewrite -(mulr_natr (f x * g x)) -(mulrC 2) mulrA mulVr ?mul1r// unitfE.
 Qed.

theories/probability.v

@@ -196,7 +196,7 @@ Lemma expectation_sum (X : seq {RV P >-> R}) :
     (forall Xi, Xi \in X -> P.-integrable [set: T] (EFin \o Xi)) ->
   'E_P[\sum_(Xi <- X) Xi] = \sum_(Xi <- X) 'E_P[Xi].
 Proof.
-elim: X => [|X0 X IHX] intX; first by rewrite !big_nil expectation_cst.
+elim: X => [|X0 X IHX] intX; first by rewrite !big_nil (expectation_cst 0).
 have intX0 : P.-integrable [set: T] (EFin \o X0).
   by apply: intX; rewrite in_cons eqxx.
 have {}intX Xi : Xi \in X -> P.-integrable [set: T] (EFin \o Xi).
@@ -230,7 +230,9 @@ have ? : 'E_P[X] \is a fin_num by rewrite fin_num_abs// integrable_expectation.
 have ? : 'E_P[Y] \is a fin_num by rewrite fin_num_abs// integrable_expectation.
 rewrite unlock [X in 'E_P[X]](_ : _ = (X \* Y \- fine 'E_P[X] \o* Y
     \- fine 'E_P[Y] \o* X \+ fine ('E_P[X] * 'E_P[Y]) \o* cst 1)%R); last first.
-  apply/funeqP => x /=; rewrite mulrDr !mulrDl/= mul1r fineM// mulrNN addrA.
+  apply/funeqP => x /=.
+  rewrite -[LHS]/((_ \* _)%R x)/= !GRing.sub_funE/= GRing.sub_funE.
+  rewrite mulrDr !mulrDl/= mul1r fineM// mulrNN addrA.
   by rewrite mulrN mulNr [Z in (X x * Y x - Z)%R]mulrC.
 have ? : P.-integrable [set: T] (EFin \o (X \* Y \- fine 'E_P[X] \o* Y)%R).
   by rewrite compreBr ?integrableB// compre_scale ?integrableZl.
@@ -459,7 +461,7 @@ rewrite varianceD/= ?varianceN ?covarianceNr ?muleN//.
 - by rewrite mulrN compreN ?integrableN.
 Qed.
 
-Lemma varianceD_cst_l c (X : {RV P >-> R}) :
+Lemma varianceD_cst_l (c : R) (X : {RV P >-> R}) :
     P.-integrable setT (EFin \o X) -> P.-integrable setT (EFin \o (X ^+ 2)%R) ->
   'V_P[(cst c \+ X)%R] = 'V_P[X].
 Proof.
@@ -480,7 +482,7 @@ have -> : (X \+ cst c = cst c \+ X)%R by apply/funeqP => x /=; rewrite addrC.
 exact: varianceD_cst_l.
 Qed.
 
-Lemma varianceB_cst_l c (X : {RV P >-> R}) :
+Lemma varianceB_cst_l (c : R) (X : {RV P >-> R}) :
     P.-integrable setT (EFin \o X) -> P.-integrable setT (EFin \o (X ^+ 2)%R) ->
   'V_P[(cst c \- X)%R] = 'V_P[X].
 Proof.

theories/realfun.v

@@ -2368,7 +2368,8 @@ have ffin: TV a x f \is a fin_num.
 have Nffin : TV a x (\- f) \is a fin_num.
   apply/bounded_variationP => //; apply/bounded_variationN.
   exact: (bounded_variationl ax xb).
-rewrite /pos_tv /neg_tv /= total_variationN -fineB -?muleBl // ?fineM //.
+rewrite /pos_tv /neg_tv /= !GRing.add_funE !GRing.opp_funE/=.
+rewrite  total_variationN -fineB -?muleBl // ?fineM //.
 - rewrite addeAC oppeD //= ?fin_num_adde_defl //.
   by rewrite addeA subee // add0e -EFinD //= opprK mulrDl -splitr.
 - by rewrite fin_numB ?fin_numD ?ffin; apply/andP; split.

theories/showcase/summability.v

@@ -15,6 +15,7 @@ Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 Import GRing.Theory Num.Def Num.Theory.
 
+Local Open Scope ring_scope.
 Local Open Scope classical_set_scope.
 
 From mathcomp Require fintype bigop finmap.