proposition: Lemma closed_ereal_le_ereal y : closed [set x | y <= x].
proof: Proof. rewrite (_ : [set x | y <= x] = ~` [set x | y > x]); last first. by rewrite predeqE=> x; split=> [rx|/negP]; [apply/negP|]; rewrite -leNgt. exact/open_closedC/open_ereal_lt_ereal. 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