proposition: Lemma nbhsr0P (P : set V) x : (\forall y \near x, P y) <-> (\forall e \near 0^'+, forall y, `|x - y| <= e -> P y).
proof: Proof. rewrite nbhs0P/= near_withinE/= !near_simpl. split=> /nbhs_norm0P[/= _/posnumP[e] /(_ _) Px]; apply/nbhs_norm0P. exists e%:num => //= r /= re yr y xyr; rewrite -[y](addrNK x) addrC. by apply: Px; rewrite /= distrC (le_lt_trans _ re)// gtr0_norm. exists (e%:num / 2) => //= r /= re; apply: (Px (e%:num / 2)) => //=. by rewrite gtr0_norm// ltr_pdivrMr// ltr_pMr// ?(ltr_nat _ 1 2). by rewrite opprD addNKr normrN ltW. 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