proposition: Lemma dyadic_itv_subU n k : [set` I n k] `<=` [set` I n.+1 k.*2] `|` [set` I n.+1 k.*2.+1].
proof: Proof. move=> r /=; rewrite in_itv /= => /andP[Ir rI]. have [rk|rk] := ltP r (k.*2.+1%:R * (2%:R ^- n.+1)); [left|right]. - rewrite in_itv /= rk andbT (le_trans _ Ir)// -muln2. rewrite natrM exprS invrM ?unitfE// ?expf_neq0// -mulrA (mulrCA 2). by rewrite divrr ?unitfE// mulr1. - rewrite in_itv /= rk /= (lt_le_trans rI)// -doubleS. rewrite -muln2 natrM exprS invrM ?unitfE// ?expf_neq0// -mulrA (mulrCA 2). by rewrite divrr ?unitfE// mulr1. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrnum ssrint interval finmap) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality fsbigop ) signed reals ereal topology normedtype sequences real_interval esum measure lebesgue_measure numfun