proposition: Lemma eqe_opp x y : (- x == - y) = (x == y).
proof: Proof. move: x y => [r| |] [r'| |] //=; apply/idP/idP => [|/eqP[->]//]. by move/eqP => -[] /eqP; rewrite eqr_opp => /eqP ->. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed