proposition: Lemma itv_bnd_infty_bigcup (R : realType) b (x : R) : [set` Interval (BSide b x) +oo%O] = \bigcup_i [set` Interval (BSide b x) (BRight (x + i%:R))].
proof: Proof. apply/seteqP; split=> y; rewrite /= !in_itv/= andbT; last first. by move=> [k _ /=]; move: b => [|] /=; rewrite in_itv/= => /andP[//] /ltW. move=> xy; exists `|ceil (y - x)|%N => //=; rewrite in_itv/= xy/= -lerBlDl. rewrite !natr_absz/= ger0_norm ?ceil_ge0 ?subr_ge0 ?ceil_ge//. by case: b xy => //= /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