proposition: Lemma itv_bnd_inftyEbigcup b x : [set` Interval (BSide b x) +oo%O] = \bigcup_k [set` Interval (BSide b x) (BLeft k%:R)].
proof: Proof. rewrite predeqE => y; split=> /=; last first. by move=> [n _]/=; rewrite in_itv => /andP[xy yn]; rewrite in_itv /= xy. rewrite in_itv /= andbT => xy; exists `|floor y|%N.+1 => //=. rewrite in_itv /= xy /=. have [y0|y0] := ltP 0 y; last by rewrite (le_lt_trans y0)// ltr_pwDr. by rewrite -natr1 natr_absz ger0_norm ?floor_ge0 1?ltW// lt_succ_floor. 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