From a895e12c3df3a91f1b6d04ceda7be9906ae677d8 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Thu, 7 Sep 2023 19:01:37 +0900 Subject: [PATCH] minor change for MathComp CI --- theories/lebesgue_integral.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v index e20b6fa3c..ff4ab41cf 100644 --- a/theories/lebesgue_integral.v +++ b/theories/lebesgue_integral.v @@ -1356,7 +1356,7 @@ have [fxn|fxn] := ltP (f x) n%:R%:E. by rewrite /A /= k2n inE; split => //=; rewrite inE/=; exists r. rewrite xAn1k mulr1 big1 ?addr0; last first. by move=> i ik2n; rewrite (disj_A0 (Ordinal k2n)) // mulr0. - rewrite -(natr1 _ k.*2) mulrDl exprS -mul2n natrM -mulf_div divrr ?unitfE//. + rewrite -(@natr1 _ k.*2) mulrDl exprS -mul2n natrM -mulf_div divrr ?unitfE//. by rewrite !mul1r ler_addl. have /orP[{}fxn|{}fxn] : ((n%:R%:E <= f x < n.+1%:R%:E) || (n.+1%:R%:E <= f x))%E.