fix

math-comp · Nov 11, 2023 · 2a71d47 · 2a71d47
1 parent 2793656
commit 2a71d47
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/theories/lebesgue_measure.v b/theories/lebesgue_measure.v
@@ -2264,7 +2264,7 @@ have finite_set_F i : finite_set (F i).
     - by move=> /= x [n Fni Bnx]; exists n => //; exists i.
   have {CFi Fir2} := le_trans MC (le_trans CFi Fir2).
   apply/negP; rewrite -ltNge lebesgue_measure_ball// lte_fin.
-  rewrite -(natr1 _ `| _ |%N) natr_absz ger0_norm ?ceil_ge0// -ltr_pdivr_mulr//.
+  rewrite -(@natr1 _ `| _ |%N) natr_absz ger0_norm ?ceil_ge0// -ltr_pdivr_mulr//.
   by rewrite -ltr_subl_addr (lt_le_trans _ (ceil_ge _))// ltr_subl_addr ltr_addl.
 have mur2_fin_num_ : mu (ball (0 : R^o) (r%:num + 2))%R < +oo.
   by rewrite lebesgue_measure_ball// ltry.