proposition: Lemma withinN (A : set R) a : within A (nbhs (- a)) = - x @[x --> within (-%R @` A) (nbhs a)].
proof: Proof. rewrite eqEsubset /=; split; move=> E /= [e e0 aeE]; exists e => //. move=> r are ra; apply: aeE; last by rewrite memNE opprK. by rewrite /= opprK addrC distrC. move=> r aer ar; rewrite -(opprK r); apply: aeE; last by rewrite -memNE. by rewrite /= opprK -normrN opprD. 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