proposition: Lemma nbhs_right0P 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 -propeqE. by apply: (@eq_near _ (nbhs (0 : R))) => y; rewrite ltrDl. 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