proposition: Lemma nbhsNe (R : realFieldType) (x : \bar R) : nbhs (- x) = [set (-%E @` A) | A in nbhs x].
proof: Proof. case: x => [r /=| |]. - rewrite /nbhs /= /ereal_nbhs -nbhs_ballE. rewrite predeqE => S; split => [[_/posnumP[e] reS]|[S' [_ /posnumP[e] reS' <-]]]. exists (-%E @` S). exists e%:num => //= r1 rer1; exists (- r1%:E); last by rewrite oppeK. by apply reS; rewrite /ball /= opprK -normrN opprD opprK. rewrite predeqE => s; split => [[y [z Sz] <- <-]|Ss]. by rewrite oppeK. by exists (- s); [exists s | rewrite oppeK]. exists e%:num => //= r1 rer1; exists (- r1%:E); last by rewrite oppeK. by apply reS'; rewrite /ball /= opprK -normrN opprD. - rewrite predeqE => S; split=> [[M [Mreal MS]]|[x [M [Mreal Mx]] <-]]. exists (-%E @` S). exists (- M)%R; rewrite realN Mreal; split => // x Mx. by exists (- x); [apply MS; rewrite lteNl | rewrite oppeK]. rewrite predeqE => x; split=> [[y [z Sz <- <-]]|Sx]; first by rewrite oppeK. by exists (- x); [exists x | rewrite oppeK]. exists (- M)%R; rewrite realN; split => // y yM. exists (- y); by [apply Mx; rewrite lteNr|rewrite oppeK]. - rewrite predeqE => S; split=> [[M [Mreal MS]]|[x [M [Mreal Mx]] <-]]. exists (-%E @` S). exists (- M)%R; rewrite realN Mreal; split => // x Mx. by exists (- x); [apply MS; rewrite lteNr | rewrite oppeK]. rewrite predeqE => x; split=> [[y [z Sz <- <-]]|Sx]; first by rewrite oppeK. by exists (- x); [exists x | rewrite oppeK]. exists (- M)%R; rewrite realN; split => // y yM. exists (- y); by [apply Mx; rewrite lteNl|rewrite oppeK]. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(fsbigop cardinality set_interval) reals signed topology constructive_ereal