proposition: Lemma nbhsDl (P : set V) (x y : V) : (\forall z \near (x + y), P z) <-> (\near x, P (x + y)).
proof: Proof. split=> /nbhs_normP[_/posnumP[e]/= Px]; apply/nbhs_normP; exists e%:num => //=. by move=> z /= xze; apply: Px; rewrite /= opprD addrACA subrr addr0. by move=> z /= xyz; rewrite -[z](addrNK y); apply: Px; rewrite /= opprB addrA. 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