proposition: Lemma bigcup_itvT {R : realType} b : \bigcup_i [set` Interval (BSide b (- i%:R)) (BRight i%:R)] = [set: R].
proof: Proof. rewrite -subTset => x _ /=; exists `|(floor `|x| + 1)%R|%N => //=. rewrite in_itv/= !natr_absz intr_norm intrD. have : `|x| < `|(floor `|x|)%:~R + 1|. by rewrite [ltRHS]ger0_norm ?lt_succ_floor// addr_ge0// ler0z floor_ge0. case: b => /=. - by move/ltW; rewrite ler_norml => /andP[-> ->]. - by rewrite ltr_norml => /andP[-> /ltW->]. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum ssrint interval) mathcomp(finmap fingroup perm rat) mathcomp(mathcomp_extra boolp classical_sets functions) HB(structures) reals ereal signed topology normedtype sequences