proposition: Lemma open_ereal_gt y : open [set r : R | y < r%:E].
proof: Proof. case: y => [y||] /=; first exact: open_gt. - rewrite (_ : [set _ | _] = set0); first exact: open0. by rewrite funeqE => ? /=; rewrite falseE. - rewrite (_ : [set _ | _] = setT); first exact: openT. by rewrite funeqE => ? /=; rewrite ltNyr trueE. 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