proposition: Lemma open_ereal_lt' x y : x < y -> ereal_nbhs x (fun u => u < y).
proof: Proof. case: x => [x|//|] xy; first exact: open_ereal_lt. - case: y => [y||//] /= in xy *; last by exists 0%R. by exists y; rewrite num_real; split => //= x ?. - case: y => [y||//] /= in xy *. + by exists y; rewrite num_real; split => //= x ?. + by exists 0%R; split => // x /lt_le_trans; apply; rewrite leey. 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