proposition: Lemma bigsetU_dyadic_itv n : `[n%:R, n.+1%:R[%classic = \big[setU/set0]_(n * 2 ^ n.+1 <= k < n.+1 * 2 ^ n.+1) [set` I n.+1 k].
proof: Proof. rewrite predeqE => r; split => [/= /[!in_itv]/= /andP[nr rn1]|]. - rewrite -bigcup_seq /=; exists `|floor (r * 2 ^+ n.+1)|%N. rewrite /= mem_index_iota; apply/andP; split. rewrite -ltez_nat gez0_abs ?floor_ge0; last first. by rewrite mulr_ge0// (le_trans _ nr). apply: (@le_trans _ _ (floor (n * 2 ^ n.+1)%:R)); last first. by apply: le_floor; rewrite natrM natrX ler_pM2r. by rewrite floor_natz intz. rewrite -ltz_nat gez0_abs; last first. by rewrite floor_ge0 mulr_ge0// (le_trans _ nr). rewrite -(@ltr_int R) (le_lt_trans (floor_le _))//. by rewrite PoszM intrM -natrX ltr_pM2r. rewrite /= in_itv /=; apply/andP; split. rewrite ler_pdivrMr// (le_trans _ (floor_le _))//. by rewrite -(@gez0_abs (floor _))// floor_ge0 mulr_ge0// (le_trans _ nr). rewrite ltr_pdivlMr// (lt_le_trans (lt_succ_floor _))//. rewrite -[in leRHS]natr1 lerD2r// -(@gez0_abs (floor _))// floor_ge0. by rewrite mulr_ge0// (le_trans _ nr). - rewrite -bigcup_seq => -[/= k] /[!mem_index_iota] /andP[nk kn]. rewrite in_itv /= => /andP[knr rkn]; rewrite in_itv /=; apply/andP; split. by rewrite (le_trans _ knr)// ler_pdivlMr// -natrX -natrM ler_nat. by rewrite (lt_le_trans rkn)// ler_pdivrMr// -natrX -natrM ler_nat. 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