proposition: Lemma nbhs_left0P x (P : set R) : (\forall y \near x^'-, P y) <-> \forall e \near 0^'+, P (x - e).
proof: Proof. rewrite !near_withinE !near_simpl nbhs0P; split=> Px. rewrite -oppr0 nearN; near=> e; rewrite ltrN2 opprK => e_lt0. by apply: (near Px) => //; rewrite gtrDl. by rewrite -oppr0 nearN; near=> e; rewrite gtrDl oppr_lt0; apply: (near Px). 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