proposition: Lemma le_wlength_itv (ndf : {homo f : x y / (x <= y)%R}) i j : {subset i <= j} -> wlength [set` i] <= wlength [set` j].
proof: Proof. set I := [set` i]; set J := [set` j]. have [->|/set0P I0] := eqVneq I set0; first by rewrite wlength0 wlength_itv_ge0. have [J0|/set0P J0] := eqVneq J set0. by move/subset_itvP; rewrite -/J J0 subset0 -/I => ->. move=> /subset_itvP ij; apply: lee_sub => /=. have [ui|ui] := asboolP (has_ubound I). have [uj /=|uj] := asboolP (has_ubound J); last by rewrite leey. rewrite lee_fin; apply: ndf; apply/le_sup => //. by move=> 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; apply/ndf/le_inf => //. 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) 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