fix

theories/lebesgue_measure.v

@@ -928,31 +928,30 @@ Proof. by rewrite ball_itv; exact: measurable_itv. Qed.
 Lemma lebesgue_measure_ball (x r : R) : (0 <= r)%R ->
   lebesgue_measure (ball x r) = (r *+ 2)%:E.
 Proof.
-rewrite le_eqVlt => /orP[/eqP <-|r0]; first by rewrite ball0 measure0 mul0rn.
+rewrite le_eqVlt => /orP[/eqP <-|r0]; first by rewrite ball0// measure0 mul0rn.
 rewrite ball_itv lebesgue_measure_itv hlength_itv/=.
 rewrite lte_fin ltr_subl_addr -addrA ltr_addl addr_gt0 //.
 by rewrite -EFinD addrAC opprD opprK addrA subrr add0r -mulr2n.
 Qed.
 
-Lemma measurable_closed_ball (x : R) r : 0 <= r -> measurable (closed_ball x r).
+Lemma measurable_closed_ball (x : R) r : measurable (closed_ball x r).
 Proof.
-rewrite le_eqVlt => /predU1P[<-|]; first by rewrite closed_ball0.
-by move=> r0; rewrite closed_ball_itv.
+have [r0|r0] := leP r 0; first by rewrite closed_ball0.
+by rewrite closed_ball_itv.
 Qed.
 
 Lemma lebesgue_measure_closed_ball (x r : R) : 0 <= r ->
   lebesgue_measure (closed_ball x r) = (r *+ 2)%:E.
 Proof.
-rewrite le_eqVlt => /predU1P[<-|r0].
-  by rewrite mul0rn closed_ball0 measure0.
+rewrite le_eqVlt => /predU1P[<-|r0]; first by rewrite mul0rn closed_ball0.
 rewrite closed_ball_itv// lebesgue_measure_itv hlength_itv/=.
 rewrite lte_fin -ltr_subl_addl addrAC subrr add0r gtr_opp// ?mulr_gt0//.
 rewrite -EFinD; congr (_%:E).
 by rewrite opprB addrAC addrCA subrr addr0 -mulr2n.
 Qed.
 
-Lemma measurable_scale_cball (k : R) c : 0 <= k -> measurable (scale_cball k c).
-Proof. by move=> k0; apply: measurable_closed_ball; rewrite mulr_ge0. Qed.
+Lemma measurable_scale_cball (k : R) c : measurable (scale_cball k c).
+Proof. exact: measurable_closed_ball. Qed.
 
 End measurable_ball.
 

theories/normedtype.v

@@ -5779,9 +5779,10 @@ End continuous.
 Section ball_realFieldType.
 Variables (R : realFieldType).
 
-Lemma ball0 (x : R) : ball x 0 = set0.
+Lemma ball0 (a r : R) : r <= 0 -> ball a r = set0.
 Proof.
-by apply/seteqP; split => // y; rewrite /ball/= ltNge normr_ge0.
+move=> r0; apply/seteqP; split => // y; rewrite /ball/=.
+by move/lt_le_trans => /(_ _ r0); rewrite normr_lt0.
 Qed.
 
 Lemma ball_itv (x r : R) : (ball x r = `]x - r, x + r[%classic)%R.
@@ -5816,9 +5817,10 @@ Qed.
 Definition closed_ball (R : numDomainType) (V : pseudoMetricType R)
   (x : V) (e : R) := closure (ball x e).
 
-Lemma closed_ball0 (R : realFieldType) (x : R) : closed_ball x 0 = set0.
+Lemma closed_ball0 (R : realFieldType) (a r : R) :
+  r <= 0 -> closed_ball a r = set0.
 Proof.
-by apply/seteqP; split => // y; rewrite /closed_ball ball0 closure0.
+by move=> r0; apply/seteqP; split => // y; rewrite /closed_ball ball0 ?closure0.
 Qed.
 
 Lemma closed_ballxx (R: numDomainType) (V : pseudoMetricType R) (x : V)