proposition: Lemma wlength_ge0 (f : cumulative R) (I : set (ocitv_type R)) : (0 <= wlength f I)%E.
proof: Proof. by rewrite -(wlength0 f) le_wlength//; exact: cumulative_is_nondecreasing. 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