proposition: Lemma Rmu_additive : semi_additive Rmu.
proof: Proof. apply/(additive2P Rmu0) => // A B /ring_finite_set[/= {}A [? _ Atriv Am ->]]. move=> /ring_finite_set[/= {}B [? _ Btriv Bm ->]]. rewrite -subset0 => coverAB0. have AUBfin : finite_set (A `|` B) by rewrite finite_setU. have AUBtriv : trivIset (A `|` B) id. move=> X Y [] ABX [] ABY; do ?by [exact: Atriv|exact: Btriv]. by move=> [u [Xu Yu]]; case: (coverAB0 u); split; [exists X|exists Y]. by move=> [u [Xu Yu]]; case: (coverAB0 u); split; [exists Y|exists X]. rewrite -bigcup_setU !Rmu_fin_bigcup//=. - rewrite fsbigU//= => [X /= [XA XB]]; have [->//|/set0P[x Xx]] := eqVneq X set0. by case: (coverAB0 x); split; exists X. - by move=> X /set_mem [|] /mem_set ?; [exact: Am|exact: Bm]. 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)