fact: Definition ereal_dnbhs (x : \bar R) : set_system (\bar R) := [set P | match x with | r%:E => r^' (fun r => P r%:E) | +oo => exists M, M \is Num.real /\ forall y, M%:E < y -> P y | -oo => exists M, M \is Num.real /\ forall y, y < M%:E -> P y end].
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(fsbigop cardinality set_interval) reals signed topology constructive_ereal