proposition: Lemma wlength_semi_additive (f : R -> R) : measure.semi_additive (wlength f).
proof: Proof. move=> /= I n /(_ _)/cid2-/all_sig[b]/all_and2[_]/(_ _)/esym-/funext {I}->. move=> Itriv [[/= a1 a2] _] /esym /[dup] + ->. rewrite wlength_itv ?lte_fin/= -EFinB. case: ifPn => a12; last first. pose I i := `](b i).1, (b i).2]%classic. rewrite set_itv_ge//= -(bigcup_mkord _ I) /I => /bigcup0P I0. by under eq_bigr => i _ do rewrite I0//= wlength0; rewrite big1. set A := `]a1, a2]%classic. rewrite -bigcup_pred; set P := xpredT; rewrite (eq_bigl P)//. move: P => P; have [p] := ubnP #|P|; elim: p => // p IHp in P a2 a12 A *. rewrite ltnS => cP /esym AE. have : A a2 by rewrite /A /= in_itv/= lexx andbT. rewrite AE/= => -[i /= Pi] a2bi. case: (boolP ((b i).1 < (b i).2)) => bi; last by rewrite itv_ge in a2bi. have {}a2bi : a2 = (b i).2. apply/eqP; rewrite eq_le (itvP a2bi)/=. suff: A (b i).2 by move=> /itvP->. by rewrite AE; exists i=> //=; rewrite in_itv/= lexx andbT. rewrite {a2}a2bi in a12 A AE *. rewrite (bigD1 i)//= wlength_itv ?lte_fin/= bi !EFinD -addeA. congr (_ + _)%E; apply/eqP; rewrite addeC -sube_eq// 1?adde_defC//. rewrite ?EFinN oppeK addeC; apply/eqP. have [a1bi|a1bi] := eqVneq a1 (b i).1. rewrite {a1}a1bi in a12 A AE {IHp} *; rewrite subee ?big1// => j. move=> /andP[Pj Nji]; rewrite wlength_itv ?lte_fin/=; case: ifPn => bj//. exfalso; have /trivIsetP/(_ j i I I Nji) := Itriv. pose m := ((b j).1 + (b j).2) / 2%:R. have mbj : `](b j).1, (b j).2]%classic m. by rewrite /= !in_itv/= ?(midf_lt, midf_le)//= ltW. rewrite -subset0 => /(_ m); apply; split=> //. by suff: A m by []; rewrite AE; exists j. have a1b2 j : P j -> (b j).1 < (b j).2 -> a1 <= (b j).2. move=> Pj bj; suff /itvP-> : A (b j).2 by []. by rewrite AE; exists j => //=; rewrite ?in_itv/= bj/=. have a1b j : P j -> (b j).1 < (b j).2 -> a1 <= (b j).1. move=> Pj bj; case: ltP=> // bj1a. suff : A a1 by rewrite /A/= in_itv/= ltxx. by rewrite AE; exists j; rewrite //= in_itv/= bj1a//= a1b2. have bbi2 j : P j -> (b j).1 < (b j).2 -> (b j).2 <= (b i).2. move=> Pj bj; suff /itvP-> : A (b j).2 by []. by rewrite AE; exists j => //=; rewrite ?in_itv/= bj/=. apply/IHp. - by rewrite lt_neqAle a1bi/= a1b. - rewrite (leq_trans _ cP)// -(cardID (pred1 i) P). rewrite [X in (_ < X + _)%N](@eq_card _ _ (pred1 i)); last first. by move=> j; rewrite !inE andbC; case: eqVneq => // ->. rewrite ?card1 ?ltnS// subset_leq_card//. by apply/fintype.subsetP => j; rewrite -topredE/= !inE andbC. apply/seteqP; split=> /= [x [j/= /andP[Pj Nji]]|x/= xabi]. case: (boolP ((b j).1 < (b j).2)) => bj; last by rewrite itv_ge. apply: subitvP; rewrite subitvE ?bnd_simp a1b//= leNgt. have /trivIsetP/(_ j i I I Nji) := Itriv. rewrite -subset0 => /(_ (b j).2); apply: contra_notN => /= bi1j2. by rewrite !in_itv/= bj !lexx bi1j2 bbi2. have: A x. rewrite /A/= in_itv/= (itvP xabi)/= ltW//. by rewrite (le_lt_trans _ bi) ?(itvP xabi). rewrite AE => -[j /= Pj xbj]. exists j => //=. apply/andP; split=> //; apply: contraTneq xbj => ->. by rewrite in_itv/= le_gtF// (itvP xabi). Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum ssrint interval) mathcomp(finmap fingroup perm rat) HB(structures) mathcomp.classical(mathcomp_extra boolp classical_sets) mathcomp.classical(functions fsbigop cardinality) reals ereal signed topology numfun normedtype sequences esum real_interval measure realfun