proposition: Lemma finite_measure_integrable_cst d (T : measurableType d) (R : realType) (mu : {finite_measure set T -> \bar R}) k : mu.-integrable [set: T] (EFin \o cst k).
proof: Proof. apply/integrableP; split; first exact/EFin_measurable_fun. have [k0|k0] := leP 0 k. - under eq_integral do rewrite /= ger0_norm//. rewrite integral_cstr//= lte_mul_pinfty// fin_num_fun_lty//. exact: fin_num_measure. - under eq_integral do rewrite /= ltr0_norm//. rewrite integral_cstr//= lte_mul_pinfty//. by rewrite lee_fin lerNr oppr0 ltW. by rewrite fin_num_fun_lty//; exact: fin_num_measure. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrnum ssrint interval finmap) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality fsbigop ) signed reals ereal topology normedtype sequences real_interval esum measure lebesgue_measure numfun