proposition: Lemma closure_lt z : closure ([set x : R | x < z]) = [set x | x <= z].
proof: Proof. rewrite eqEsubset; split. by rewrite closureE; apply: smallest_sub => // ? /ltW. move=> v; rewrite /mkset le_eqVlt => /predU1P[<-{z}|]; last first. by move=> ?; exact: subset_closure. move=> B [e /= e0 vB]; near (0 : R)^'+ => d. exists (v - d); split; rewrite /= ?gtrDl ?oppr_lt0//; apply: vB => /=. by rewrite opprB addrC addrNK gtr0_norm//; near: d. Unshelve. all: by end_near. 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