proposition: Lemma not_near_at_rightP T (f : R -> T) (p : R) (P : pred T) : ~ (\forall x \near p^'+, P (f x)) -> forall e : {posnum R}, exists2 x, p < x < p + e%:num & ~ P (f x).
proof: Proof. move=> pPf e; apply: contrapT => /forallPNP pePf; apply: pPf; near=> t. apply: contrapT; apply: pePf; apply/andP; split. - by near: t; exact: nbhs_right_gt. - by near: t; apply: nbhs_right_lt; rewrite ltrDl. 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