proposition: Lemma ereal_dnbhs_le_finite (R : numFieldType) (r : R) : ereal_dnbhs r%:E --> nbhs r%:E.
proof: Proof. by move=> P [_/posnumP[e] reP] //=; exists e%:num => //= ? ? ?; exact: reP. Qed.
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