proposition: Lemma eset1Ny : [set -oo] = \bigcap_k `]-oo, (-k%:R%:E)[%classic :> set (\bar R).
proof: Proof. rewrite eqEsubset; split=> [_ -> i _ |]; first by rewrite /= in_itv /= ltNyr. move=> [r|/(_ O Logic.I)|]//. move=> /(_ `|floor r|%N Logic.I); rewrite /= in_itv/= ltNge. rewrite lee_fin; have [r0|r0] := leP 0%R r. by rewrite (le_trans _ r0) // lerNl oppr0 ler0n. rewrite lerNl -abszN natr_absz gtr0_norm; last first. by rewrite ltrNr oppr0 floor_lt0. by rewrite mulrNz lerNl opprK floor_le. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum ssrint interval) mathcomp(finmap fingroup perm rat) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality fsbigop) reals ereal signed topology numfun normedtype HB(structures) sequences esum measure real_interval realfun exp lebesgue_stieltjes_measure