proposition: Corollary Corollary4_eq : p != empty_intpart -> \sum_(i <- rem_corners p) (HLF (decr_nth_intpart p i)) = HLF p.
proof: Proof. Proof using. move=> /Corollary4; rewrite -mulr_suml => /divr1_eq <-. apply eq_big_seq => i; rewrite mem_filter => /andP[Hi _]. by rewrite /= Hi. Qed.
imports: Misc Ccpo mathcomp(all_ssreflect) mathcomp(ssrint div rat ssralg ssrnum) tools subseq partition Yamanouchi stdtab Qmeasure