proposition: Lemma le_hlength_itv i j : {subset i <= j} -> hlength [set` i] <= hlength [set` j].
proof: Proof. set I := [set` i]; set J := [set` j]. have [->|/set0P I0] := eqVneq I set0; first by rewrite hlength0 hlength_itv_ge0. have [J0|/set0P J0] := eqVneq J set0. by move/subset_itvP; rewrite -/J J0 subset0 -/I => ->. move=> /subset_itvP ij; apply: leeB => /=. have [ui|ui] := asboolP (has_ubound I). have [uj /=|uj] := asboolP (has_ubound J); last by rewrite leey. by rewrite lee_fin le_sup // => r Ir; exists r; split => //; apply: ij. have [uj /=|//] := asboolP (has_ubound J). by move: ui; have := subset_has_ubound ij uj. have [lj /=|lj] := asboolP (has_lbound J); last by rewrite leNye. have [li /=|li] := asboolP (has_lbound I); last first. by move: li; have := subset_has_lbound ij lj. rewrite lee_fin lerNl opprK le_sup// ?has_inf_supN//; last exact/nonemptyN. move=> r [r' Ir' <-{r}]; exists (- r')%R. by split => //; exists r' => //; apply: ij. 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