proposition: Lemma punct_eitv_Nybnd b y : [set` Interval -oo%O (BSide b y%:E)] = [set -oo%E] `|` EFin @` [set x | x \in Interval -oo%O (BSide b y)].
proof: Proof. rewrite predeqE => x; split; rewrite /= in_itv. - move: x => [x| |] yxb; [|by case: b yxb|by left]. by right; exists x => //; rewrite in_itv /= andbT; case: b yxb. - move=> [->|[r]]. + by case: b => /=; rewrite ?(ltNyr, leNye). + by rewrite in_itv /= => yxb <-; case: b yxb. 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