proposition: Lemma dnbhsN {R : numFieldType} (r : R) : (- r)%R^' = (fun A => -%R @` A) @` r^'.
proof: Proof. apply/seteqP; split=> [A [e/= e0 reA]|_/= [A [e/= e0 reA <-]]]. exists (-%R @` A). exists e => // x/= rxe xr; exists (- x)%R; rewrite ?opprK//. by apply: reA; rewrite ?eqr_opp//= opprK addrC distrC. rewrite image_comp (_ : _ \o _ = idfun) ?image_id// funeqE => x/=. by rewrite opprK. exists e => //= x/=; rewrite -opprD normrN => axe xa. exists (- x)%R; rewrite ?opprK//; apply: reA; rewrite ?eqr_oppLR//=. by 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