proposition: Lemma wlength_itv_ge0 (ndf : {homo f : x y / (x <= y)%R}) i : 0 <= wlength [set` i].
proof: Proof. rewrite wlength_itv; case: ifPn => //; case: (i.1 : \bar _) => [r| |]. - by rewrite suber_ge0// => /ltW /(le_er_map ndf). - by rewrite ltNge leey. - case: (i.2 : \bar _) => //=; last by rewrite leey. by move=> r _; rewrite leey. 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