proposition: Lemma nbhsNimage (R : numFieldType) (x : R) : nbhs (- x) = [set -%R @` A | A in nbhs x].
proof: Proof. rewrite nbhsN /fmap/=; under eq_set => A do rewrite preimageEinv//= inv_oppr. by rewrite (eq_imageK opprK opprK). 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