proposition: Lemma itv_bnd_open_bigcup (R : realType) b (r s : R) : [set` Interval (BSide b r) (BLeft s)] = \bigcup_n [set` Interval (BSide b r) (BRight (s - n.+1%:R^-1))].
proof: Proof. apply/seteqP; split => [x/=|]; last first. move=> x [n _ /=] /[!in_itv] /andP[-> /le_lt_trans]; apply. by rewrite ltrBlDr ltrDl invr_gt0 ltr0n. rewrite in_itv/= => /andP[sx xs]; exists `|ceil ((s - x)^-1)|%N => //=. rewrite in_itv/= sx/= lerBrDl addrC -lerBrDl. rewrite -[in X in _ <= X](invrK (s - x)) ler_pV2. - rewrite -natr1 natr_absz ger0_norm; last first. by rewrite ceil_ge0// invr_ge0 subr_ge0 ltW. by rewrite (@le_trans _ _ (ceil (s - x)^-1)%:~R)// ?lerDl// ceil_ge. - by rewrite inE unitfE ltr0n andbT pnatr_eq0. - by rewrite inE invr_gt0 subr_gt0 xs andbT unitfE invr_eq0 subr_eq0 gt_eqF. 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