proposition: Lemma itv_open_bnd_bigcup (R : realType) b (r s : R) : [set` Interval (BRight s) (BSide b r)] = \bigcup_n [set` Interval (BLeft (s + n.+1%:R^-1)) (BSide b r)].
proof: Proof. have /(congr1 (fun x => -%R @` x)) := itv_bnd_open_bigcup (~~ b) (- r) (- s). rewrite opp_itv_bnd_bnd/= !opprK negbK => ->; rewrite image_bigcup. apply eq_bigcupr => k _; apply/seteqP; split=> [_/= [y ysr] <-|x/= xsr]. by rewrite oppr_itv/= opprD. by exists (- x); rewrite ?oppr_itv//= opprK// negbK opprB opprK addrC. 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