proposition: Lemma le_hlength : {homo hlength : A B / (A `<=` B) >-> A <= B}.
proof: Proof. move=> a b /le_Rhull /le_hlength_itv. by rewrite (hlength_Rhull a) (hlength_Rhull b). 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