proposition: Lemma wlength_itv i : wlength [set` i] = if i.2 > i.1 then g i.2 - g i.1 else 0.
proof: Proof. case: ltP => [/lt_ereal_bnd/neitvP i12|]; first by rewrite /wlength set_itvK. rewrite le_eqVlt => /orP[|/lt_ereal_bnd i12]; last first. rewrite -wlength0; congr (wlength _). by apply/eqP/negPn; rewrite -/(neitv _) neitvE -leNgt (ltW i12). case: i => -[ba a|[|]] [bb b|[|]] //=. - rewrite /= => /eqP[->{b}]; move: ba bb => -[] []; try by rewrite set_itvE wlength0. by rewrite wlength_singleton. - by move=> _; rewrite set_itvE wlength0. - by move=> _; rewrite set_itvE wlength0. 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