From 08c782b0d72a8ce2b0793fa07eeedac29e803d2f Mon Sep 17 00:00:00 2001 From: Quentin Vermande Date: Mon, 4 Nov 2024 14:32:00 +0100 Subject: [PATCH] adapt to mc#1256 --- altreals/realseq.v | 2 +- classical/cardinality.v | 2 +- reals/constructive_ereal.v | 2 +- theories/derive.v | 19 +++++++++++-------- theories/esum.v | 3 ++- theories/ftc.v | 15 +++++++++------ theories/landau.v | 8 ++++---- theories/lebesgue_integral.v | 17 ++++++++++------- theories/lebesgue_measure.v | 17 +++++++++++------ theories/probability.v | 10 ++++++---- theories/realfun.v | 3 ++- theories/showcase/summability.v | 1 + 12 files changed, 59 insertions(+), 40 deletions(-) diff --git a/altreals/realseq.v b/altreals/realseq.v index f8d1d909e..3eee73bb1 100644 --- a/altreals/realseq.v +++ b/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. diff --git a/classical/cardinality.v b/classical/cardinality.v index c84602f5f..d072a5622 100644 --- a/classical/cardinality.v +++ b/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 _ := diff --git a/reals/constructive_ereal.v b/reals/constructive_ereal.v index a2155ef0e..f9992483c 100644 --- a/reals/constructive_ereal.v +++ b/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). diff --git a/theories/derive.v b/theories/derive.v index 2cd1198f7..c12691955 100644 --- a/theories/derive.v +++ b/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. diff --git a/theories/esum.v b/theories/esum.v index 57959228b..f624b90d2 100644 --- a/theories/esum.v +++ b/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. diff --git a/theories/ftc.v b/theories/ftc.v index 4f553f2c1..dbd38cc91 100644 --- a/theories/ftc.v +++ b/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:=@GRing.opp 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:=@GRing.opp 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:=@GRing.opp 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:=@GRing.opp 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:=@GRing.opp 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. diff --git a/theories/landau.v b/theories/landau.v index bee296e96..41641a440 100644 --- a/theories/landau.v +++ b/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. diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v index b043af47c..449e4efa8 100644 --- a/theories/lebesgue_integral.v +++ b/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:=@GRing.opp 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:=@GRing.opp 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:=@GRing.opp 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. diff --git a/theories/lebesgue_measure.v b/theories/lebesgue_measure.v index e658b9a26..4331f353d 100644 --- a/theories/lebesgue_measure.v +++ b/theories/lebesgue_measure.v @@ -1001,14 +1001,18 @@ 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:=@GRing.opp 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. @@ -1016,7 +1020,8 @@ move=> mf mg; rewrite (_ : (_ \* _) = (fun x => 2%:R^-1 * (f x + g x) ^+ 2) 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. diff --git a/theories/probability.v b/theories/probability.v index c57cac324..3c94d0d62 100644 --- a/theories/probability.v +++ b/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. diff --git a/theories/realfun.v b/theories/realfun.v index bb902bfa2..6d63f7edd 100644 --- a/theories/realfun.v +++ b/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. diff --git a/theories/showcase/summability.v b/theories/showcase/summability.v index dae60a5b9..86eacd112 100644 --- a/theories/showcase/summability.v +++ b/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.