proposition: Lemma lebesgue_measure_closed_ball (x r : R) : 0 <= r -> lebesgue_measure (closed_ball x r) = (r *+ 2)%:E.
proof: Proof. rewrite le_eqVlt => /predU1P[<-|r0]; first by rewrite mul0rn closed_ball0// measure0. rewrite closed_ball_itv// lebesgue_measure_itv/= lte_fin -ltrBlDl addrAC. rewrite subrr add0r gtrN// ?mulr_gt0// -EFinD; congr (_%:E). by rewrite opprB addrAC addrCA subrr addr0 -mulr2n. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum ssrint interval) mathcomp(finmap fingroup perm rat) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality fsbigop) reals ereal signed topology numfun normedtype HB(structures) sequences esum measure real_interval realfun exp lebesgue_stieltjes_measure