proposition: Lemma content_sub_additive : sub_additive mu.
proof: Proof. move=> X A n Am Xm XA; pose B i := A\_`I_n i `&` X. have XE : X = \big[setU/set0]_(i < n) B i. rewrite -big_distrl/= setIidr// => x /XA/=. by rewrite -!bigcup_mkord => -[k nk Ax]; exists k; rewrite // patchT ?inE. have Bm i : measurable (B i). case: (ltnP i n) => ltin; last by rewrite /B patchC ?inE ?set0I//= leq_gtF. by rewrite /B ?patchT ?inE//; apply: measurableI => //; apply: Am. have subBA i : B i `<=` A i. by rewrite /B/patch; case: ifP; rewrite // set0I//= => _ ?. have subDUB i : seqDU B i `<=` A i by move=> x [/subBA]. have DUBm i : measurable (seqDU B i : set (SetRing.type T)). apply: measurableD; first exact: sub_gen_smallest. by apply: bigsetU_measurable => ? _; apply: sub_gen_smallest. have DU0 i : (i >= n)%N -> seqDU B i = set0. move=> leni; rewrite -subset0 => x []; rewrite /B patchC ?inE/= ?leq_gtF//. by case. rewrite -SetRing.RmuE// XE bigsetU_seqDU measure_bigsetU//. rewrite [leRHS](big_ord_widen n (mu \o A))//= [leRHS]big_mkcond/=. rewrite lee_sum => // i _; case: ltnP => ltin; last by rewrite DU0 ?measure0. rewrite -[leRHS]SetRing.RmuE; last exact: Am. by rewrite le_measure ?inE//=; last by apply: sub_gen_smallest; apply: Am. Qed.
imports: mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality fsbigop ) reals ereal signed topology normedtype sequences esum numfun HB(structures)