proposition: Lemma set1_bigcap_oc (R : realType) (r : R) : [set r] = \bigcap_i `]r - i.+1%:R^-1, r]%classic.
proof: Proof. apply/seteqP; split=> [x ->|]. by move=> i _/=; rewrite in_itv/= lexx ltrBlDr ltrDl invr_gt0 ltr0n. move=> x rx; apply/esym/eqP; rewrite eq_le (itvP (rx 0%N _))// andbT. apply/ler_addgt0Pl => e e_gt0; rewrite -lerBlDl ltW//. have := rx `|floor e^-1%R|%N I; rewrite /= in_itv => /andP[/le_lt_trans->]//. rewrite lerD2l lerN2 -lef_pV2 ?invrK//; last by rewrite posrE. by rewrite -natr1 natr_absz ger0_norm ?floor_ge0 ?invr_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