proposition: Lemma near_shift {K : numDomainType} {R : normedModType K} (y x : R) (P : set R) : (\near x, P x) = (\forall z \near y, (P \o shift (x - y)) z).
proof: Proof. rewrite propeqE; split=> /= /nbhs_normP [_/posnumP[e] ye]; apply/nbhs_normP; exists e%:num => //= t et. apply: ye; rewrite /= !opprD addrA addrACA subrr add0r. by rewrite opprK addrC. have /= := ye (t - (x - y)); rewrite addrNK; apply. by rewrite /= opprB addrCA addrA subrK. 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