proposition: Lemma itv_infty_bnd_bigcup (R : realType) b (x : R) : [set` Interval -oo%O (BSide b x)] = \bigcup_i [set` Interval (BLeft (x - i%:R)) (BSide b x)].
proof: Proof. have /(congr1 (fun x => -%R @` x)) := itv_bnd_infty_bigcup (~~ b) (- x). rewrite opp_itv_bnd_infty negbK opprK => ->; rewrite image_bigcup. apply eq_bigcupr => k _; apply/seteqP; split=> [_ /= -[r rbxk <-]|y/= yxkb]. by rewrite oppr_itv/= opprB addrC. by exists (- y); [rewrite oppr_itv/= negbK opprD opprK|rewrite opprK]. 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