proposition: Lemma nbhsN (R : numFieldType) (x : R) : nbhs (- x) = -%R @ x.
proof: Proof. rewrite predeqE => A; split=> //= -[] e e_gt0 xeA; exists e => //= y /=. by move=> ?; apply: xeA => //=; rewrite -opprD normrN. by rewrite -opprD normrN => ?; rewrite -[y]opprK; apply: xeA; rewrite /= 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