proposition: Lemma open_ereal_gt' x y : y < x -> ereal_nbhs x (fun u => y < u).
proof: Proof. case: x => [x||] //=; do ?[exact: open_ereal_gt]; case: y => [y||] //=; do ?by exists 0. - by exists y; rewrite num_real. - by move=> _; exists 0%R; split => // x; apply/le_lt_trans; rewrite leNye. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrint ssrnum finmap matrix) mathcomp(rat interval zmodp vector fieldext falgebra) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality set_interval Rstruct) ereal reals signed topology prodnormedzmodule