proposition: Lemma lebesgue_measure_itv (i : interval R) : lebesgue_measure ([set` i] : set R) = (if i.1 < i.2 then (i.2 : \bar R) - i.1 else 0)%E.
proof: Proof. move: i => [[x a|[|]]] [y b|[|]]. by rewrite lebesgue_measure_itv_bnd wlength_itv. - by rewrite set_itvE ?measure0. - by rewrite lebesgue_measure_itv_bnd_infty/= ltry. - by rewrite lebesgue_measure_itv_infty_bnd/= ltNyr. - by rewrite set_itvE ?measure0. - by rewrite lebesgue_measure_itv_infty_infty. - by rewrite set_itvE ?measure0. - by rewrite set_itvE ?measure0. - by rewrite set_itvE ?measure0. 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