proposition: Lemma closure_gt z : closure ([set x | z < x] : set R) = [set x | z <= x].
proof: Proof. rewrite eqEsubset; split. by rewrite closureE; apply: smallest_sub => // ? /ltW. move=> v; rewrite /mkset le_eqVlt => /predU1P[<-{v}|]; last first. by move=> ?; exact: subset_closure. move=> B [e /= e0 zB]; near (0 : R)^'+ => d. exists (z + d); split; rewrite /= ?ltrDl//; apply: zB => /=. by rewrite opprD addNKr normrN gtr0_norm//. 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